问题标签 [satisfiability]

我正在寻找用 java 实现的 GSAT 和 SA-SAT 算法。有人知道吗？谢谢你。

SMT-Solver 可用于约束求解。众所周知，CSP 求解器多年来也用于约束求解。那么 SMT 求解器相对于 CSP 求解器的优势是什么？

SMT 求解器是为处理类似于 SAT 的可满足性而开发的。众所周知，SAT 也是可满足性的，并且提出了 SAT 的变体。其中之一是 max-SAT。所以我想问一下是否存在 max-SMT 求解器，如果存在，它是如何工作的？

我有一个布尔公式：(x_{1} or x_{2}) and (x_{3} or x_{4}) and ..... and (x_{2r-1} or x_{2r}) ,其中x_{i}属于集合：{p_{1}, p_{2}, ... p_{99} , ~p_{1}, ~p_{2}, ... ~p_{99} }我必须确定给定公式的某些x_{i}值是否为真。

我知道它通常在计算上很困难。但是有什么非常快速的方法可以解决这个特殊问题吗？到目前为止，我已经尝试过回溯——即在递归中，我为每个可能的变量替换了每个可能的值（0 或 1，所以不是很多），并且每个尚未获得值的变量都是微不足道的。在深入递归之前，我会检查公式（即使不是每个变量都有值），如果它是假的，我不会更深入。但它太慢了。有任何想法吗？我将非常感谢您的帮助。

我写了一个我认为非常有趣的问题的答案，但不幸的是，在我发布之前，该问题已被其作者删除。我在这里重新发布问题的摘要和我的答案，以防它可能对其他人有用。

假设我有一个 SAT 求解器，给定一个联合范式的布尔公式，它返回一个解（满足公式的变量赋值）或问题不可满足的信息。

我可以使用这个求解器找到所有的解决方案吗？

给定一组s公式，我想找到一个最小的子集s'，s它暗示s. 我称之为s最小独立集，因为对于 中的每一对a,b，并不意味着s'，反之亦然。 ab

在我看来，天真的方法需要O(2^|s|)复杂性。有没有更有效的方法？能否对这个问题进行编码，以利用当前的 smt/sat 求解器（例如 unsat 核心）？

假设您有一个 CNF 公式，其中一些变量标记为特殊。
有没有办法让 SAT Solver（比如 minisat）找到一个解决方案，最大化分配给 true 的特殊变量的数量？

给定一个 m*n 二进制矩阵 A，m*p 二进制矩阵 B，其中 n > m 计算 X 使得 AX=B 的有效算法是什么？

例如：

请注意，当我说二进制矩阵时，我指的是在字段 Z_2 上定义的矩阵，也就是说，所有算术都是模 2。

如果有任何兴趣，这是我在为随机纠错码生成合适的矩阵时面临的问题。

这是我的问题，我在 Matlab 中遇到了 SAT 问题（满意度）

实际上我需要一个名为 DPLL 的函数，我在这里的某个地方看到了它，但它是在 java 中，有人可以帮我吗？

我正在尝试寻找解决问题的实用方法（例如，在工程方面），其中我有一堆未知值：

和一个表达式二叉树（在内存中），最终返回一个布尔值，例如

我拥有的布尔运算符and or xor not和 32 位整数有比较之类的东西，以及加法、乘法、除法（注意：这些必须尊重 32 位溢出！）以及一些按位的东西（移位、按位 &、| ^)。但是，我不一定需要支持所有这些操作 [参见：LOL_NO_IDEA]

我想得到三个答案之一：

• ES_POSSIBLE [我不需要知道如何，只是被告知存在一种可能]
• 不可能 [无论我的变量持有什么值，这个等式永远不会是真的]
• LOL_NO_IDEA [这是可以接受的，如果问题太复杂或耗时]

我要解决的问题都不是太大或太复杂，术语太多（最多是数百个）。并且拥有大量的 LOL_NO_IDEA 很好。然而，我正在解决数以百万计的此类问题，因此持续的成本会让人感到痛苦（例如，转换为文本格式，并调用外部求解器）

由于我是从 scala 执行此操作的，因此使用 SAT4J 看起来非常吸引人。虽然，文档很糟糕（特别是像我这样的人，他只研究了这个 SAT 世界几天）

但我目前的想法是首先将所有 Int32 转换为 32 个布尔值。这样，我可以通过将其作为嵌套布尔表达式来表达（a < b）之类的关系（比较 msb，如果它们是 eq，则为下一个，等等）

然后当我有一个布尔变量和布尔表达式的大表达式树时——然后遍历它，同时逐步建立一个： http ://en.wikipedia.org/wiki/Conjunctive_normal_form

然后将其输入SAT4J。

然而，所有这些看起来都非常具有挑战性——甚至构建 CNF 似乎也非常低效（以天真的方式进行，我会实现它）并且容易出错。更不用说尝试将所有整数数学编码为布尔表达式。而且我还没有找到为像我这样的人设计的好资源

我会很感激任何反馈，即使它就像“大声笑，你是个白痴——看看 X”或“是的，你的想法是正确的。享受吧！”