gophersat下载 - gophersat源代码下载

gophersat

Ai源码

1.0.0

下载

Gophersat，用 Go 编写的 SAT 和伪布尔求解器

这是 Gophersat，一个纯粹用 Go 编写的 SAT 和伪布尔求解器。 Gophersat 由阿图瓦大学 CRIL（Centre de Recherche en Informatique de Lens）和 CNRS 开发。它是在 MIT 许可下发布的。 Gophersat 相当高效，即在典型的 SAT 基准测试中，它的运行速度比它受到强烈启发的顶级求解器（即葡萄糖或 minisat）慢约 2 到 5 倍。它还可以解决 MAXSAT 问题以及伪布尔决策和优化问题。

版本 1.4：切割平面

Gophersat 的最后一个稳定版本是 1.4 版。它包括可选的切割平面求解策略。

有些问题，例如著名的鸽巢问题，需要很长时间才能使用纯逻辑推理来解决。

鸽笼问题可以这样表达：是否可以将n只鸽子放入m个鸽子中，其中m = n-1，而不将几只鸽子放入同一个洞中并将所有鸽子放入一个洞中？答案很明显：如果你有 4 只鸽子在 3 个洞里，你不能把它们全部放在不同的洞里。但你如何证明这一点呢？ SAT 或 PB 求解器将通过尝试所有可能的组合来证明这一点，并且可能的组合的数量呈指数增长。因此，尝试解决 n=20 的问题在实践中是不可行的，尽管该问题有明显的答案。

一些 PB 求解器实施另一种策略：割平面策略。本文不会详细描述，但这种策略在某些问题上可以非常有效，例如无法通过纯逻辑推理有效解决的鸽巢问题，但在大多数问题上会比较慢。

现在可以将切割平面与 Gophersat 一起使用。只需使用-cp命令行选项即可。因此，不要调用：

 gophersat problem.opb

只需致电：

 gophersat -cp problem.opb

1.3版

Gophersat 的最后一个稳定版本是 1.3 版。这是一个小更新，增加了在处理 MAXSAT 问题时访问底层求解器的能力。

版本 1.2：可解释的 AI：UNSAT 认证、MUS 提取

Gophersat 1.2 版包括一种理解 UNSAT 实例的方法，既可以在问题为 UNSAT 时提供 RUP 证书，也可以提供提取公式中不可满足的子集的能力。还修正了一些错误，并改进了对增量 SAT 求解的支持。

要了解有关这些功能的更多信息，您可以查看有关 UNSAT 证书和 MUS 的教程。

要使用 gophersat 可执行文件生成证书，只需调用：

 gophersat -certified problem.cnf

然后，证书将使用 RUP 符号打印在标准输出上。证书是动态生成的，因此请注意，即使问题实际上可以解决，也会生成部分无用的证书。这是社区中的常见做法，虽然生成的子句是无用的噪音，但实际上这不是问题。

要从 UNSAT 实例中提取 MUS，只需调用：

 gophersat -mus problem.cnf

MUS 将打印在标准输出上。如果问题不是 UNSAT，则会显示错误消息。

目前，这些工具仅适用于纯 SAT 问题（即不是伪布尔问题）。

1.1版

自 1.1 版本以来，Gophersat 包含一个新的、更高效的纯 SAT 问题核心求解器和一个处理 MAXSAT 问题的包。它还包括一个用于优化和模型计数的新 API，一旦发现新模型，就会将其写入通道。

关于 Gophersat 中的版本号

自 1.0 版本以来，Gophersat 的 API 被认为是稳定的，这意味着该 API 保证保持向后兼容，直到发生主要版本转变。换句话说，如果您的程序适用于 1.0 版本的 gophersat，它仍然适用于 1.1 或更高版本，但不一定适用于 2.0 以上版本。

请注意，“仍然工作”只是指“将编译并产生相同的输出”，而不是“在内存或时间方面具有相同的性能”。这是一个重要的区别：在次要版本升级期间，可以引入新的启发式方法或数据类型，这意味着某些给定的问题可以比以前更快或更慢地解决。

我该如何安装它？

go get github.com/crillab/gophersat && go install github.com/crillab/gophersat

解决 SAT 问题

Gophersat 可以用作独立求解器（读取 DIMACS CNF 文件）或用作任何 go 程序中的库。

要解析 DIMACS 文件，您可以使用以下语法调用 gophersat：

 gophersat --verbose file.cnf

其中--verbose是可选参数，使求解器在求解过程中显示信息。

Gophersat 还能够读取和解决更通用的布尔公式，而不仅仅是以用户不友好的 DIMACS 格式表示的问题。它还本身处理基数约束，即必须至少有 n 个文字为 true 的子句，其中 n > 1。

解决伪布尔问题

Gophersat 可以用作独立求解器（读取 OPB 文件）或用作任何 go 程序中的库。

要解决伪布尔问题（无论是决策问题还是优化问题），您可以使用以下语法调用 gophersat：

 gophersat --verbose file.opb

其中--verbose是可选参数，使求解器在求解过程中显示信息。

目前，它只能解决所谓的 DEC-SMALLINT-LIN 问题和 OPT-SMALLINT-LIN，即决策问题（是否有解），用于小整数的线性约束（加权文字的总和） (n < 2^30)，或优化问题（最佳解决方案是什么，最小化给定的成本函数），用于小整数的线性约束。

解决 MAXSAT 问题

得益于maxsat软件包，Gophersat 现在可以解决 MAXSAT 问题。

要解决加权 MAXSAT 问题，您可以使用以下语法调用 gophersat：

 gophersat --verbose file.wcnf

其中--verbose是可选参数，使求解器在求解过程中显示信息。该文件应该以（WCNF 格式）[http://www.maxsat.udl.cat/08/index.php?disp=requirements] 表示。

什么是 SAT 求解器？ SAT考试的问题是什么？

SAT 代表布尔可满足性问题 (Boolean Satisfiability Problem) ，是典型的 NP 完全问题，即在最坏情况下不存在不花费指数时间的已知解决方案的问题。简而言之，SAT 求解器尝试为给定的命题公式找到使其所有变量都成立的赋值（如果存在这样的赋值）。

虽然使用朴素算法实现 SAT 求解器很简单，但这种实现在实践中效率非常低。 Gophersat 实现了最先进的功能，因此非常高效，使其可在需要高效推理引擎的 Go 程序中实际使用。

尽管出于实际原因这并不总是最佳决定，但任何 NP 完全问题都可以转化为 SAT 问题并由 Gophersat 解决。此类问题包括旅行商问题、约束规划、背包问题、规划、模型检查、软件正确性检查等。

有关 SAT 问题的更多信息，请参阅维基百科有关 SAT 的文章。

您还可以在教程“SAT for noobs”中找到有关如何表示您自己的布尔公式的信息，以便 gophersat 可以使用它们。

什么是 MAXSAT？

MAXSAT 是 SAT 决策问题的优化等价物。纯 SAT 求解器将返回满足所有子句的模型，如果不存在此类模型，则返回 UNSAT，而 MAXSAT 求解器将返回满足尽可能多的子句的模型。

部分和加权 MAXSAT

MAXSAT 有扩展。

部分MAXSAT意味着，虽然我们希望满足尽可能多的子句，但无论如何，有些子句（称为硬子句）必须满足。因此，部分 MAXSAT 问题可以被认为是不可满足的。

例如，为学校生成时间表是一个部分 MAXSAT 问题：既有软性问题（例如，我们希望下午 4 点之后开始的课程尽可能少），也有硬性问题（两名教师不能同时在两个不同的地方）同时）的限制。

加权 MAXSAT意味着条款与成本相关：尽管是可选的，但某些条款被认为比其他条款更重要。例如，如果子句 C1 的成本为 3，而子句 C2 和 C3 的成本均为 1，则满足 C1 但既不满足 C2 也不满足 C3 的解决方案将被认为比满足 C2 和 C3 但不满足 C1 的解决方案更好，所有其他解决方案事物是平等的。

部分加权MAXSAT是指问题中同时存在软子句和硬子句，并对软子句进行加权。在这方面，“纯”MAXSAT 是更通用的部分加权 MAXSAT 的特殊情况：“纯”MAXSAT 问题是部分加权 MAXSAT 问题，其中所有子句都是与权重 1 关联的软子句。

那么伪布尔问题呢？

在某种程度上，伪布尔问题是 SAT 问题的概括：任何命题子句都可以写成单个伪布尔约束，但表示伪布尔约束可能需要指数数量的命题子句。

（线性）伪布尔表达式是这样的表达式：

 w1 l1 + w2 x2 + ... + wn xn ≥ y

其中y和所有wi都是整数常量，所有li都是布尔文字。

例如，如果以下表达式为真

 2 ¬x1 + x2 + x3 ≥ 3

布尔变量x1必须为 false，并且x2和x3至少其中之一必须为 true。这相当于命题公式

 ¬x1 ∧ (x2 ∨ x3)

伪布尔表达式是命题子句的概括：任何子句

 x1 ∨ x2 ∨ ... ∨ xn

可以重写为

 x1 + x2 + ... + xn ≥ 1

伪布尔问题的描述可能比其对应的命题问题小得多，但解决伪布尔问题仍然是 NP 完全的。

Gophersat 解决了决策问题（该问题是否有解决方案）和优化问题。优化问题是与成本函数相关的伪布尔问题，即必须最小化的项之和。 gophersat 不只是尝试找到满足给定约束的模型，而是尝试找到保证既满足约束又最小化成本函数的模型。

在搜索最优解的过程中，gophersat 一旦找到就会提供次优解（即解决所有约束但尚不能保证最优的解），因此用户可以在给定时间内得到次优解限制，或者等待更长时间以获得有保证的最佳解决方案。

Gophersat 快吗？为什么要使用它？

是和不是。它比简单的实现要快得多，足以用于解决现实世界的问题，但比顶级、高度优化、最先进的求解器慢。

Gophersat 的目标并不是成为最快的 SAT/PB 求解器。目标是让地鼠能够访问 SAT 和 PB 技术，而无需借助用其他语言（通常是 C/C++）编写的求解器的接口。

然而，在某些情况下，与用另一种语言编写的求解器连接是您的应用程序的最佳选择。如果您有很多小问题需要解决，Gophersat 将是最快的选择。对于更大的问题，如果您想以解决问题时间为代价，尽可能减少依赖性，Gophersat 也不错。如果您需要解决难题并且不介意使用 cgo 或使用外部程序，那么 Gophersat 可能不是最佳选择。

Go 中还有其他一些 SAT 求解器，主要是 go-sat 和 gini。根据我们运行的测试，Gini 的性能与 Gophersat 相当，尽管平均速度稍慢一些。

Gophersat 还提供了其他求解器所不具备的炫酷功能（例如，用户友好的输入格式），因此它可以用作描述和解决 NP 难题的工具，这些问题可以轻松简化为 SAT/PB问题。