问题标签 [satisfiability]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
2 回答
759 浏览

constraint-programming - 真实世界的 SAT 实例

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

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

0 投票
1 回答
139 浏览

z3 - 剂量 SMTLIB 1.2 具有(获取值)功能,如 SMTLIB 2

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

谢谢

0 投票
1 回答
114 浏览

optimization - LTL 公式的 SAT

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

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

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

非常感谢!

0 投票
1 回答
648 浏览

z3 - Z3 SAT Solver 的随机种子

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

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

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

针对Z3CryptominisatClasp的较小问题的测量(每个求解器和排序模式运行 100 次测试):

在此处输入图像描述

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

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

0 投票
1 回答
477 浏览

complexity-theory - 库克定理(简单英语)

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

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

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

0 投票
1 回答
570 浏览

optimization - minisat 如何有效地找到所有 SAT 解决方案

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

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

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

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

谢谢。

0 投票
0 回答
418 浏览

c++ - CVC4:在 C++ 接口中使用量词

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

相反,我只是收到一条错误消息:

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

编辑(问https://www.andrew.cmu.edu/user/liminjia/):

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

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

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

在 C++ 中,我们有

0 投票
2 回答
3910 浏览

algorithm - 从 SAT 转换为 3-SAT

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

0 投票
1 回答
173 浏览

declarative - SAT接地工具?

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

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

并从中生成一个 DIMACS 文件?

一般来说,SAT竞赛实例是如何产生的?

0 投票
1 回答
689 浏览

satisfiability - CNF 与喇叭可满足性

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