问题标签 [satisfiability]

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

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

我想知道是否SMTLIB1.2有等价于SMTLIB2's ( get-value)。我正在使用and运行不同的SMT编码测试，问题出在输出中，我不断获取模型与 100 多个辅助变量值混合的所有值。Z3 SMT solverSMTLIB1.2

谢谢

SAT 求解器证明命题公式 F 的可满足性。但是，是否可以使用 SAT 来测试 LTL 公式的可满足性？例如，我们能证明下面的 LTL 公式是不可满足的吗？

G (A => B) 和 (A = True) 和 (B = False)

如果您能指出可以处理此问题的 SAT 求解器，那就太好了。

非常感谢！

我正在使用Z3作为格式SAT solver编码的棘手可满足性问题。CNF/DIMACS

将输入随机化以增加找到解决方案的机会是否有意义：

• 打乱 CNF 子句的顺序
• 对输入变量的编号进行排序/打乱

针对Z3、Cryptominisat和Clasp的较小问题的测量（每个求解器和排序模式运行 100 次测试）：

对于Z3，对于我的示例而言，排序/随机化看起来并不乐观，这可能不具有代表性。

我还没有找到影响 SAT 模块的随机种子命令行参数Z3。参数“random_seed”似乎只控制 SMT 求解器。

我在算法课程中阅读了 Garey 和 Johnson 所著的Computers and Intractability - A Guide to the Theory of NP-Completeness 一书；然而，在一年后复习这些材料时，我意识到我从来没有真正理解过库克定理。

关于证明，我理解为什么 SAT 首先被证明是 NP 的（NP 完全的第一个要求），但是我正在努力通过显示“遗传”多项式下的“其他”NP 完全问题的技术性转换为 SAT。

我想知道是否有人可以以更淡化的方式解释这一点，这可能会澄清对本节的额外阅读。

我找到了一种使用此链接中描述的方式查找所有解决方案的方法。

这工作正常，但速度很慢。因为它从一开始就重新计算约束，所以 i_e 没有利用以前的计算。

现在，我在这个 链接中看到，有一种更有效的方法可以使用 MiniSat 作为库来查找所有解决方案。但是那里没有描述方法。

您能否为我指出正确的文档以有效地找到所有 SAT 解决方案？

谢谢。

我试图弄清楚如何使用 C++ 接口在 CVC4 中编写量词。这是我试图运行但不能运行的示例。

相反，我只是收到一条错误消息：

但我将量词定义为forall. 我做错了什么？

编辑（问https://www.andrew.cmu.edu/user/liminjia/）：

语法错误。我们想知道是否

是真是假。但如果上述公式有效与否，CVC4 则不会，因为 SMT 求解器不是成熟的一阶逻辑定理证明器。

如果您想尝试一些可行的方法，请尝试使用 CVC4 语言：

在 C++ 中，我们有

有谁知道一个好的程序可以将每个子句具有任意数量的变量的 CNF 文件转换为每个子句恰好有 3 个变量的 CNF 文件（3-CNF）？我在计算机科学书籍中看到过这种算法，但在任何地方都找不到实现，如果其他人已经完成了，我不想浪费时间自己实现它。谢谢！

在 ASP（答案集编程）中，程序是用更高级别的声明性语言编写的，然后以确定性的方式接地，以使用诸如 lparse 或 gringo 之类的接地程序生成 ASP 实例。

SAT 社区是否有流行的grounders 用于生成实例？换句话说，有没有可以采用如下表达式的东西：

并从中生成一个 DIMACS 文件？

一般来说，SAT竞赛实例是如何产生的？

我知道证明喇叭公式是否可满足更容易。我的问题是：为什么使用喇叭公式而不是普通 CNF 更容易？