使用实数自动推理

Question

我有大量的等效性，看起来像：

$（a \ leq 0.54 \ wedge b \ geq 0.12）\ vee（c \ gt 0.98）$ $ \ LeftrightArrow $ $（x \ leq 0.25）\ Vee（x \ gt 0.91 \ wedge y \ ge 0.01）$

这只是一个例子。通常，等效左侧或右侧的公式可以是采用析出性正常形式（DNF）条款的形式的任何东西，这些数字可以是具有固定精度的任何实数，并且不等式标志可能是<跨度class=“math-container”> $ \ leq $ ， $ \ lt $ ， $ \ geq $ ，或 $ \ gt $ 。

重要的是，所有公式的左侧可能的变量（这里 $ \ {a，b，c \} $ ）表单这与所有公式右侧的可能变量不同（这里 $ \ {x，y，z \} $ ）。两侧可能有任何固定数量的变量：不需要是3个变量，并且在任一侧时不需要是相同的数字。

我还有一些形式的含义：

$（a \ leq 0.32 \ wedge b \ geq 0.62）$ $ \ lightarrow $ < SPAN Class=“Math-Container”> $（C \ GT 0.00）$

在这里，左侧和右侧都只是不平等的连词，但重要的是，在左侧和右侧的变量集，即 $ \ {a，b，c \} $ 这里，与仅在前一种公式的左侧的变量集（即等价性）的左侧相同。

我的问题是：我需要什么样的自动推理员来找到一套此类公式的逻辑后果？我只是在寻找一个具体的识别，这属于这一般的问题，以及任何可能可用的箱子的任何开箱设备。也许这是一个smt问题？

Answer 1

是的，可以使用支持线性实际算法的SMT求解器来解决此问题。然而，SMT支持更多的常规不等式，您可以在其中具有线性和变量的线性和（例如， $ 2a + 3x \ Le 5.7 $ ）而不是单个变量和a之间的简单比较常量（例如， $ a \ le 1.6 $ ），因此它可能比您需要更强大，所以如果您没有任何涉及SUM的线性不等式，那么我同意假名，即最好的方法可以使用SAT求解器。

我会建议稍微不同的编码到饱和。而不是一个热的编码，其中 $ x_i $ 表示 $ c_ {i-1} \ le x \ le C_I $ ，我建议一个略有不同的编码： $ x_i $ 表示 $ x \ le c_i $ < / span>。因此，而不是编码到 $（x_1，\ dots，x_n）$ 矢量，如 $（0,0,0， 1,0）$ 您将编码为 $（1,1,1,1,0）$ 。您添加了 $ x_i \意味着x_ {i-1} $ ，然后每个不等式 $ x \ le c_i $ 对应于布尔变量 $ x_i $ 。

Answer 2

在您的情况下，最简单的解决方案可能是使用SAT。

您的第一个子句包括 $ x \ le 0.25 $ 和 $ x> 0.91 $ 。这意味着变量 $ x $ 有五个感兴趣区域，我们用布尔变量标识： $ 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，\ idty）$ 。

为每个范围创建一个布尔变量，并将子句转换为使用它们。因此，例如， $ x \ le 0.25 $ 将转换为 $ x_1 \ vee x_2 $ ，以及 $ x <0.91 $ 将转换为 $ x_1 \ vee x_2 \ vee x_3 $ 。

更多条款意味着更多的常量，因此对原始变量的更多感兴趣的范围。