问题标签 [satisfiability]

我想知道编码一个布尔公式需要多少位

@ 是 SAT 的一个实例。我认为它是 4 位，因为可能组合的总数是 2（power4）。那是对的吗？我应该计算 OR、NOT 和 AND 来计算编码所需的位数吗？我搜索了很多，但在这方面找不到任何东西。

我正在尝试解决仅包含单热约束的 SAT 问题。现在我正在使用 Claessen 在 Sec. 中提出的 one-hot 编码。[1] 的 4.2 和 MiniSAT。

我想知道是否有解决此类问题的更好方法，例如与基于 CNF 的 SAT 求解器相比，一类求解器更适合此类问题。我搜索了一下，但根本找不到关于 SAT 和 one-hot 约束的太多信息。

[1]成功的 SAT 编码技术。马格努斯·比吉尔克。2009 年 7 月 25 日

我知道有几部作品试图处理 SMT 中的理论组合。但是，SMT-Lib 2.0 语言 ( http://smtlib.cs.uiowa.edu/docs.html ) 没有说明这一点。我的问题是它是否支持这一点，以及什么 Solvers 提供了同时处理多种理论的能力？

谢谢，

请考虑以下 3-SAT 实例和相应的图表

图表可以用其他两种形式显示

该图的 Tutte 多项式为

图的独立数为 4，则考虑的 3-SAT 实例是可满足的。使用以下代码检查这一事实：

相应的输出是：

图的对应补码是

并且图的补码的 Tutte 多项式是

补集的团数是 4，然后它表示所考虑的 3-SAT 实例是可满足的。

问题是：是否可以使用 Tutte 多项式来确定所考虑的 3-SAT 实例是否可满足？

这是问题：

考虑体育联赛调度问题的以下规则和定义：

• N（偶数）支球队，每两支球队在赛季中恰好交手一次。
• 赛季持续 (N-1) 周。
• 每支球队在赛季的每个星期都打一场比赛。
• 每周有 N/2 个时段或时段；每个时段都安排在一场比赛中。

(a) (25 分) 将体育联赛调度问题编码为布尔可满足性问题。提示：

• 为了模拟两个不同的球队在给定的插槽中互相比赛，将每个插槽分成两个子插槽。对于每周，我们有 N 个子插槽。采用这样的惯例，即两支球队打连续的子时段——一个奇数的子时段，然后是一个偶数的子时段——实际上是在互相比赛。
• 变量 Xijk 被分配为真，当且仅当球队 i 在第 k 周在子槽 j 中比赛时
• 变量 Yijk 被赋值为真，当且仅当当队 i 在第 k 周与队 j 比赛时

有一个问题：给出说明每个子槽中只有一支球队参加比赛的条款。有多少条语句？

我的问题：这里的“条款”实际上是什么意思？我发布这个问题是希望有人能告诉我这个问题想问什么，我不是在寻找直接的解决方案。

谢谢，如果有人可以帮忙。

从 API：

我查看了文档，但找不到任何详细信息。我应该选择什么值？有比随机测试更好的猜测吗？后者可能需要几天时间，因为我的执行时间一次运行长达 24 小时。

我实际上使用“pycosat”为picosat 的python 绑定。

PS：有人可以添加“picosat”标签吗？

布尔可满足性问题是用于检查布尔表达式可满足性的概括。现在布尔表达式由多项式的非负性算法生成。例如，多项式可以是并且具有某个区间，例如变量的数量在哪里。我目前使用特殊算法（例如分支定界算法）检查多项式的特征，例如非负性，在这种算法中，我将大问题转化为较小的问题，但缺少一些 SAT 求解器（例如MiniSat ）承诺的学习功能。所以

1. 一些 SAT 求解器旨在检查多项式的属性，例如多线性函数或一般多元函数？

2. 将多元函数和非负性算法转换为布尔表达式的任何简单方法？

今天我也想研究一下在 haskell 中解决 SAT 的选项。首先，我想为 picosat 求解器编写自己的界面。

然后我发现那里有SBV 库。它是 Z3、Yices、CVC4 和 Boolector 的接口。

此外，我在 github 上进行了谷歌搜索，结果发现甚至有可用的Picosat 绑定。

考虑到快速/高性能的限制，是否有任何其他与 SAT 求解器相关的 Haskell 绑定值得关注。Carification：适用于高性能 SAT 解决（例如，运行数天的问题，以及需要尽快完成的问题，因为我检查了 2^20 或更多 SAT 问题）。例如，我在 hackage 中特别缺少的是与 Plingeling 等快速并行 SAT 求解器的绑定。（另外，我偶然发现了 github 上当前更新的 picosat 绑定，我很可能会错过其他选项）

SBV 库的默认选项是 Z3 SMT 求解器。我的有根据的猜测是否正确，即 picosat 比 Z3 更快地解决普通 SAT 问题？

我正在尝试使用SAT Solver来解决组合问题。

这涉及以下步骤：

1. 将问题编码为一组布尔表达式。
2. 将表达式的连词翻译成CNF/DIMACS
   （使用自制工具bc2cnf、bool2cnf或Limboole）
3. 求解CNF
   （使用 SAT 求解器，如Cryptominisat、Plingeling、Clasp或Z3）
4. 将解决方案（假设为“SAT”结果）转换回问题域

这适用于我的小样本。但对于更具挑战性的问题，SAT 求解器需要数小时甚至数天才能得出 SAT/UNSAT 结论。我尝试调整我的编码以获得解决方案。但是我在编码上投入的精力越多，我就越不能确定我的编码实际上是正确的（即“可满足性等效”）。

从布尔表达式到 CNF 的步骤相当复杂，在可管理数量的子句和变量方面是有效的。等待 SAT 求解器的时间很长并且不确定时间是否花在正确的轨道上是很痛苦的。

布尔表达式可能是错误的。因此，我想验证 CNF 实际上代表了原始问题，而不仅仅是布尔表达式。

我的问题：

我如何验证给定的编码是原始布尔表达式的有效表示？

从文献中，我知道了一些问题的解决方案，我可以将其转化为变量分配，以获得对我的编码过程的信任。但是由于Tseitin encoding，我的 CNF 中的大多数变量都是辅助（切换）变量。如果没有Tseitin encoding，我的 CNF 将太大而无法解决。因此，我不能简单地检查已知解决方案是否满足每个 CNF 子句。

我曾尝试使用cnf2aig将 CNF 转换回布尔表达式，但该工具仍处于起步阶段。在不切换变量的情况下，可以直接根据主要问题变量的布尔表达式检查分配。

有一些关于“CNF 到电路”方法的出版物，但没有一个提供可用的工具。

是否有任何最佳实践来完成这样的检查？

GSAT（贪婪可满足性）算法可用于找到以 CNF 编码的搜索问题的解决方案。我知道，由于 GSAT 是贪婪的，它是不完整的（这意味着可能存在解决方案但 GSAT 找不到它的情况）。从下面的链接中，我了解到，当翻转变量贪婪地将我们困在 I → I' → I'' → I 这样的循环中时，就会发生这种情况。

http://www.dis.uniroma1.it/~liberato/ar/incomplete/incomplete.html

我一直在努力想出一个可以显示这一点的实际实例，但一直未能（也无法在其他地方找到示例）。任何帮助将非常感激。谢谢 ：）

PS 我不是在谈论变量与子句的比率接近 4.3 的“硬”k-SAT 问题。我只是在寻找一个简单的例子，可能涉及最少数量的变量和/或所需的子句。