用SAT解决析取线性算术问题
摘要：析取线性算术（DLA）是一种被几乎所有现有定理证明器支持的重要可决理论。该理论由形式为$Sigma\_{j=1}^{n}a\_jcdot x\_j \le b$的谓词的布尔组合组成，其中系数$a\_j$，上界$b$和变量$x\_1 >... x\_n$类型为实数($mathbb{R}$)。我们利用傅立叶-莫茨金消元将析取线性算术简化为命题逻辑。尽管该过程的复杂度与竞争技术不相上下，但在解决验证问题方面具有实际优势。它还促进了将多个理论归约为此逻辑进行决策的选择。实验证明，当公式中存在许多析取时，该方法相对于现有技术具有很强的优势。
作者：Ofer Strichman
论文ID：cs/0402002
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23