真实世界的 SAT 实例答案

【问题标题】：real world SAT instances真实世界的 SAT 实例
【发布时间】：2014-07-20 14:24:01
【问题描述】：

我正在设计和实现一个 SAT 求解器。如果所有子句都采用这种形式会特别好

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

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

【问题讨论】：

Fahem Bacchus 在利用 SAT 和 QBF 求解中的电路表示方面做了大量工作。这似乎与您正在尝试做的事情非常相关。

标签： constraint-programming satisfiability operations-research

【解决方案1】：

你提出了一个有效的观点。 Peter Stuckey 在SAT Conference 2013 上做了一个“没有 CNF 问题”的演讲。你会发现幻灯片here。

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

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

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

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

关于 CNF 有几点值得一提：

CNF（DIMACS 格式）可以被许多工具处理
CNF 相当紧凑
CNF 可以很容易地解析

【讨论】：

【解决方案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/~barrett/smtlib/QF_UF_Hierarchy.zip

SMT 比赛分为逻辑组。所以有可能在只支持QF_UF的比赛中加入求解器。（其实OpenSMT2求解器只支持QF_UF，参与了SMT-COMP 2014。）

【讨论】：