Raciocínio automatizado com números reais

Question

Eu tenho um grande número de equivalências que se parecem com:

$(a \leq 0.54 \cunha b \geq 0.12) \vee (c \gt 0.98)$ $\Leftrightarrow$ $(x \leq 0.25) \vee (x \gt 0.91 \cunha y \geq 0.01)$

Este é apenas um exemplo.Em geral, as fórmulas no lado esquerdo ou direito da equivalência pode ser qualquer coisa que toma a forma de uma forma normal disjuntiva (DNF) cláusula, os números poderiam ser quaisquer números reais com uma precisão fixa, e os sinais de desigualdade poderia ser $\leq$, $\lt$, $\geq$, ou $\gt$.

O que é importante é que as variáveis possíveis no lado esquerdo de todas as fórmulas (aqui $\{a, b, c\}$) formam um conjunto que é diferente de variáveis possíveis no lado direito de todas as fórmulas (aqui $\{x, y, z\}$).Pode haver qualquer número fixo de variáveis em ambos os lados:não precisa ser de 3 variáveis, e não precisa ser um número igual de ambos os lados.

Eu também tenho algumas implicações do formulário:

$(a \leq 0.32 \cunha b \geq 0.62)$ $ ightarrow$ $c \gt 0.00)$

Aqui ambos os lados esquerdo e direito são apenas conjunções de desigualdades, mas o que é importante é que o conjunto de variáveis em ambos os lados direito e esquerdo, i.é. $\{a, b, c\}$ aqui, é o mesmo que o conjunto de variáveis em apenas o lado esquerdo do anterior, uma espécie de fórmula (i.e.as equivalências).

A minha pergunta é:que tipo de automatizado italiano, seria preciso encontrar a conseqüência lógica de um conjunto de tais fórmulas?Eu estou apenas olhando para um concreto de identificação da classe geral de problemas que este pertence, e qualquer fora-da-caixa de pensadores que podem estar disponíveis.Talvez este seja um SMT problema?

Answer 1

Sim, você pode resolver isso com um SMT solver que suporta linear real aritmética.No entanto SMT suporta mais geral de desigualdades, onde você pode ter linear soma de variáveis (por exemplo, $2a+3x \le 5.7$) em vez de simples comparações entre uma única variável e uma constante (por exemplo, $a \le 1.6$), portanto, pode ser mais poderoso do que você precisa, então, se você não tem qualquer linear desigualdades envolvendo somas, então eu concordo com o Pseudônimo que pode ser a melhor abordagem para uso do SAT solver.

Eu gostaria de sugerir um pouco diferente de codificação para o SAT.Em vez de um quente codificação, onde $x_i$ significa que $c_{i-1} \le x \le c_i$, Eu gostaria de sugerir um pouco diferente de codificação: $x_i$ significa $x \le c_i$.Assim, em vez de codificação para um $(x_1,\dots,x_n)$ vetor como $(0,0,0,1,0)$ você poderia codificar para $(1,1,1,1,0)$.Adicionar restrições que $x_i \implica x_{i-1}$, e , em seguida, cada desigualdade $x \le c_i$ corresponde a uma variável booleana $x_i$.

Answer 2

No seu caso, a solução mais simples pode ser para uso do SAT.

Seu primeiro cláusula inclui $x \le 0.25$ e $x > 0.91$.Isto significa que há cinco regiões de interesse para a variável $x$, que identificamos com variáveis booleanas: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in (0.91,\infty)$.

Criar uma variável booleana para cada um destes intervalos, e converter a cláusula de usá-los.Assim, por exemplo, $x \le 0.25$ gostaria de converter para $X_1 \vee X_2$, e $x < 0.91$ gostaria de converter para $X_1 \vee X_2 \vee X_3$.

Mais cláusulas significaria mais constantes, e, portanto, mais intervalos de interesse para uma variável primitiva.