1

我正在设计和实现一个 SAT 求解器。如果所有条款都具有以下形式，那就特别好

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

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

4

2 回答 2

3

你提出了一个有效的观点。Peter Stuckey 在2013 年 SAT 会议上做了一个演讲“没有 CNF 问题” 。您可以在此处找到幻灯片。

对于实际应用，最好有像 Stuckey 的MiniZinc这样的高级问题描述语言。在 CNF 中对问题进行编码通常很乏味且容易出错。

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

科学市场上有很多求解器“学校”可以减少问题编码的问题。例如 Gringo/ Clasp之类的答案集编程 (ASP) 和MiniZinc 之类的约束编程求解器 (CSP) 。

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

关于 CNF，有几点值得一提：

  1. CNF（以 DIMACS 格式）可以由许多工具处理
  2. CNF 相当紧凑
  3. CNF 可以很容易地解析
于 2014-07-21T22:49:35.447 回答
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)

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

SMT-LIB QF_UF 基准包含此格式中的大量问题（6647 个“精心制作”和 3 个“工业”）：

SMT 比赛分为逻辑部分。因此，可以在仅支持 的比赛中输入求解器QF_UF。（其实OpenSMT2求解器只支持QF_UF并参与了SMT-COMP 2014。 ）

于 2014-12-22T08:38:12.037 回答