真实世界的SAT实例

Question

我正在设计和实现一个SAT求解器。如果所有子句的格式都是

，那就更好了。

a AND b = c
a OR b = c
a XOR b = c
a = NOT b

在文献中，他们使用CNF形式，我认为这在实践中对原始现实世界问题的表示效率较低。他们这样做是因为现有的SAT求解器可以更好地处理CNF。然而，这并不适用于我的SAT解决方案，这将对我造成不公平的劣势。有人知道上述形式的任何现实世界实例吗?

Answer 1

你提出了一个有效的观点。Peter Stuckey在2013年SAT会议上做了题为"There Are No CNF Problems"的演讲。你可以在这里找到幻灯片。

对于实际应用来说，最好有一个像Stuckey的MiniZinc这样的高级问题描述语言。在CNF中对问题进行编码通常非常繁琐且容易出错。

回答你的问题
是的，大多数现实世界的问题都被描述为布尔或数学表达式，而不是CNF。需要一个编码步骤来让它们被求解器求解。

在科学市场上有很多解决方案"学校"，使问题编码不那么成问题。例如Gringo/Clasp之类的答案集编程(ASP)和MiniZinc之类的约束规划求解器(CSP)。

另一种选择是使用"Circuit-SAT"而不是CNF-SAT。"电路"是用逻辑门和它们之间的连接来描述的。这是一种布尔表达式的嵌套系统。我最喜欢的将电路转换成CNF的工具是bc2cnf。

有一些关于CNF的优点:

1. CNF (DIMACS格式)可以由许多工具处理
2. CNF相当紧凑
3. CNF可以很容易地解析

Answer 2

SAT求解器的理论和应用与CNF表示紧密耦合。如果你的求解器使用布尔公式而不是CNF，你可能不想把你的求解器看作是一个"SAT求解器"，而是一个"除了量词自由一阶逻辑之外不支持任何理论的SMT求解器"。

许多SMT求解器支持SMT- libv2作为输入语言。在SMT-LIB中，求解器的功能集是通过使用set-logic语句设置"逻辑"来配置的。QF_UF逻辑只支持基本的没有量词的布尔公式，应该与您想要的相同。例如，SMT-LIB语法中的示例子句:

(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(assert (= (and a b) c))
(assert (= (or a b) c))
(assert (= (xor a b) c))
(assert (= a (not b)))
(check-sat)
(exit)

当传递给SMT求解器时，将打印unsat。

SMT-LIB QF_UF基准测试包含大量这种格式的问题(6647"精心制作"和3"工业"):

• http://www.cs.nyu.edu/巴雷特/smtlib QF_UF_Hierarchy.zip

SMT竞赛按逻辑划分。因此，可以在只支持QF_UF的竞赛中输入求解器。(实际上，OpenSMT2求解器只支持QF_UF，并参与了SMT-COMP 2014。)