问题标签 [sat]

对于我开始的项目，我需要使用 SAT 求解器。我以前使用过其中一些，但主要用于实验，而这里项目的主要限制是良好的性能。我正在尝试寻找替代方案，并尝试了解每种替代方案如何针对我的特定要求进行定位。尤其是：

1. 我需要提取令人满意的分配，不仅检查可满足性，而且求解器应该允许我重复求解相同的公式，寻找不同的可能令人满意的分配，最终以有效的方式迭代所有这些（例如，没有我必须添加一个子句并重新开始）。

2. 该项目应该仍然得到积极维护和相当的生产质量，而不是自出版以来放弃的一些赢得竞争的研究项目（见picosat）。

3. 此外，由于我使用的是 C++，所以求解器应该提供一个高效且（可能）良好的书面 C++ 接口。

我考虑的第一个候选人是 Z3，但我对文档感到困惑，无法理解是否支持上面的第 1 点，并且考虑到我只需要 SAT 而不是 SMT，这是否可能是矫枉过正。C++ 接口似乎也很容易使用，但我无法忍受我必须用纯字符串命名变量的事实（这与我周围的算法非常糟糕。这不是可以避免的吗？）。

那么你能给我一些关于使用哪个 SAT 求解器的建议，或者通过对 Z3 的疑问来阐明一些观点吗？

我有一个 AIG（和逆变器图），我一直在修改它，我需要使用 Z3 以增量方式检查其可满足性。我可以生成 AIG 的 CNF 表示，并且理想情况下希望将这些子句直接提供给求解器并从我的代码中重复调用它。有什么方法可以通过 C/C++ API 直接向 Z3 求解器添加子句（或 AIG）？

我目前正在尝试使用 SAT 求解器来解决难题“Kuromasu”，该求解器采用常见的 DIMACS 格式，即作为连接范式 (CNF) 的输入。

在 Kuromasu 中，您有一个带有 mxn 单元的矩形板。一个细胞要么是黑色的，要么是白色的。游戏的目标是决定哪个单元格是哪种颜色。一些单元格包含一个数字。包含数字的单元格始终为白色。该数字告诉您应该从该单元格中看到多少个单元格，包括其自身。同一行和同一列中的所有白色单元格都是可见的，直到第一个黑色单元格。

示例 5x4 网格，# 表示黑色单元格：

我需要制定这个约束，以 SAT 求解器理解的方式找到黑色区域的位置。我已经能够通过遍历编号单元格左侧、右侧、顶部、底部的所有单元格并检查将它们着色为黑色是否满足约束来为每个数字生成一个分离范式 (DNF) 版本。这给了我一份 DNF 中可能的黑细胞星座列表。我通过在每个单元格中引入一个变量来对游戏进行编码，如果为假，则为黑色，如果为真，则单元格为白色。以下是上述字段的所有变量（1 索引，因为 DIMACS 格式将假变量指定为负整数，将真变量指定为正对应）：

仅对于上面示例中的 2-number 约束，我将生成以下内容：

(-4 & -15) | (-3 & -10) (等式 1.)

这代表了可以遵循约束的两种方式。但是，要将其输入到 SAT-Solver，我需要将 (Eq 1.) 转换为 CNF。我实现了一个（简单的）转换器，它可以工作，但由于转换为 CNF的复杂性，它确实很慢且内存密集。对于有超过 4 种方式来实现它们的约束，这样做是不可行的。

如何以可以直接提供给 Solver 的方式制定约束？可能吗？这个问题我想了好久，还是搞不明白。

谢谢！

我有一个布尔公式（格式：CNF），我使用 Z3 SAT 求解器检查其可满足性。当公式可满足时，我有兴趣获得部分分配。我尝试model.partial=true了一个简单的OR门公式，但没有得到任何部分分配。

你能建议如何做到这一点吗？我对分配没有任何限制，除了它是部分的。

我正在尝试使用 Choco 4.0.1 对 SAT 公式进行建模。我阅读了文档，我试图从javadoc中理解，但不幸的是我到目前为止失败了。这是我第一次处理这些类型的问题，也是 choco。所以，我可能会问一些非常明显的问题。

我需要向模型添加一些约束，例如（每个 var 都是 BoolVar）：

我正在尝试在模型中使用 ifOnlyIf 方法，但我不知道如何否定变量或使用 and。有人可以（理想情况下）为我提供一些示例代码或有关如何对这些类型的约束进行建模的任何想法吗？

我之前没有用过SAT求解器，所以我开始学习如何使用SAT4J。大多数情况下，我使用它的 API，但有时我发现很难理解某些参数（在类或方法中）的含义或它们的格式/类型是可以接受的。例如：

我的问题是是否有一些使用示例，可​​以帮助我更多地理解 SAT4j 中实现的功能？

先感谢您！

我正在用 SAT 建模一个问题，并尝试用cryptominisat解决它。如果没有约束，我想给我的变量一个默认值。

我浏览了手册，set_default_polarity似乎是答案。我试过了，但它没有像我预期的那样工作。我真的不明白polarity这里的术语。一些谷歌搜索并没有帮助我，因为我不熟悉逻辑。

所以，我的问题是：

1. 您能否解释一下什么polarity是或向我指出一些入门级的资源？

2. cryptominisat（或通常在 SAT 求解器中）是否有接口来设置逻辑变量的默认值？这种功能的术语是什么？

谢谢。

我在 .dimacs/.cnf 文件中有一个公式，如下所示：

是否可以在 SAT4j 中仅提取那些包含变量 2、3 和 4 的子句？然后，我只需要检查这组新子句的一致性，即：

我尝试使用 Assumptions，我尝试使用 Constraints，但我仍然找不到这样做的方法。

谢谢你的任何建议。

编辑

我认为有一种类似的方法solver.addClause(clause)，但反过来solver.getClause(clause)......虽然，我正在为求解器提供 .cnf 文件中的子句。

编辑 2

首先，假设与子句具有相同的语法，

但变量conjunctions在假设和disjunctions子句中。这是一个区别。正确的？我的测试示例是这样说的。（我只需要获得额外的批准）。

其次，我使用选择器变量的问题是：

一个简单的公式a V b有三个模型：

当我添加一个选择器变量时，例如 ，s并且它的假设是-s，那么我有相同数量的模型，即 3 个模型：

当假设为true时，即 ，s那么我有 4 个模型，而不是我想要的 0：

当然是什么时候s = T，那么(s V a V b) = (T V a V b) = T，但这是对子句的一种删除方式(a V b)吗？我需要的是模型的数量，真实的模型！有没有办法在以某种方式“删除”我们希望通过假设排除的这些变量（即a和）时找到确切的模型？b

对于这种情况，这是我当前在 Scala 中的代码：

感谢您的任何帮助。

假设变量数 N 和子句数 K 相等。找到一种算法，该算法返回满足子句的不同方式的数量。

我读到SAT与独立集有关。

相关：CNF 简化（事实上，我认为该问题的提交者可能一直在追求我想要的东西）

存在许多用于简化（或求解前“预处理”）DIMACS 格式 CNF 公式的工具，并且大多数 SAT 求解器都包含一些工具。然而，我所知道的一切都将一个平凡可满足的公式简化为一个具有零个或一个变量的平凡可满足的 CNF，即它们只试图保持公式的可满足性。我至少尝试过 SatELite 和 cryptominisat 的预处理模式。

然而，对于构建一个大问题的 CNF，在我看来，一次简化一个明确定义的问题子集会非常有用，然后可能会在最终的 CNF 中重复很多次，并添加额外的这些子公式中的一些变量之间的约束。

那么，是否存在任何工具，或者普通 SAT 求解器（或其他求解器，如 Z3，我用来生成我想最小化的 CNF）以某种方式巧妙地使用，以简化 CNF 公式，同时保留所有解决方案wrt一组给定的变量？