问题标签 [sat-solvers]
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.
java - 是否有易于使用的 java 0-1 IP 求解器？
我想使用 0-1 整数规划求解器作为 java 程序中的工具。我在网上找不到任何易于使用的东西。我尝试了 sat4j 的伪布尔库，但这没有很好的记录，有些类与 API 中的描述不一致（有些方法签名不同）。
你有什么建议吗？
z3 - 使用 Z3 和位向量理论获取半字节的函数
我正在尝试学习一些关于 z3 和位向量理论的知识。我的意图是创建一个函数来从位向量的位置获取半字节
此代码返回半字节：
问题是我想避免多次ite调用。我试图将 ((_ extract 3 0) l) 替换为 ((_ extract (+ 4 idx) idx l) 之类的东西，但它不起作用。
谢谢
PS：这个想法是从命令行使用z3（不使用任何库）。
c# - 使用 Z3 和 c# 获取 Unsat 核心示例
我正在尝试在 C# 实现中使用 Z3 sat 求解器。这段代码非常接近微软自己在“ http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs ”中给出的示例。我的代码是：
但是当我到达这个模型的“s.UnsatCore”时，它仍然是空的。
我也尝试过输入这样的断言：
我希望 UnsatCore 返回“constraint1，constint3”。谁能帮我解决我做错了什么？
python - 解析 dimacs CNF 文件 python
我有一个 DIMACS cnf 格式的文件，我需要将其处理为 SAT Solver 所需的格式。
具体来说，我需要得到：
至
谢谢您的帮助！
satisfiability - CNF 与喇叭可满足性
我知道证明喇叭公式是否可满足更容易。我的问题是：为什么使用喇叭公式而不是普通 CNF 更容易？
python - 当公式应该满足时，Z3 求解器返回 unsat
我得到了一个 Z3 求解器（python 接口）似乎无法处理的“简单”公式。它运行了相当长的一段时间（30 分钟）然后返回未知，即使我可以在一分钟内手动找到令人满意的任务。这是公式：
它可能看起来有点吓人，但让我带您了解一下。<uc ij> 都是整数变量。我首先指定它们应该是 0 或 1，然后我引入了一个约束，即它们中的一个应该是 1，而其他的应该是 0（使用总和）。
在第二部分中，您可以忽略所有或基本上只是将每个变量的搜索空间限制为 [-1000, 1000]。然后我有最内在的约束，这应该意味着： < uc 0.2> = 1 < uc 1.0> = 1 < uc 2.1> = 1 和所有其他 = 0。就是这样。我很确定求解器应该能够解决这个问题，但没有运气。我可以将总和约束更改为类似 Or(< uc 1.0>,< uc 1.1>,< uc 1.2>) 的东西，这很有趣，在这种情况下解决了我的问题（求解器在几秒钟内返回正确的分配），但总的来说，这显然，不等于我想要的。
问题：
- 有没有类似的东西，我可以用它来代替整数？
- 一些推荐的方式来表达一个参数恰好是 1 的事实？
- 在不改变公式的第二部分的情况下，可以通过其他一些方法来解决这个问题。
非常感谢！
// 编辑：在玩了几个选项之后，我通过在 ForAll 条件之后放置边条件来“解决”它（只是交换两行代码）。这根本不应该有什么不同，但现在他在 0.5 秒内找到了正确的分配 - 什么？我还尝试了使用 4 个变量 (a,b,c,d) 代替 (a,b,c) 的示例，但它又运行了几个小时......有帮助吗？也用长度和/或改变总和不起作用。
random - SAT 求解：DPLL 与？
现在我正在写关于解决 SAT 的文章，但我被困在了一个点上。我希望你能帮助我。
我想描述一些解决 SAT 问题的方法。现在我有三种不同的方法：
- 蛮力
- 随机（天真）
- DPLL（具有不同的启发式）
- ? 失踪 ？
- ...
我的问题是唯一有效的算法是 DPLL（以及其他一些与 DPLL 略有不同的算法）。因此我没有什么可以比较 DPLL 的。
我的问题：如果您能告诉我一些不基于 DPLL (DP) 的算法，我可以将其与之进行比较，那就太好了。
以下是我发现的一些，但无法确定它们是否是一个不错的选择，或者是否有更好的选择：
- 莫尼恩-斯佩肯迈尔
- Dantsin、Goerdt、Hirsch 和 Schöning
- Paturi-Pudlák-Zane-算法
- 霍夫迈斯特、舍宁、舒勒和渡边
谢谢你的帮助。
sat-solvers - SAT 求解器，0 深度作业
在谈论 SAT 求解器时，例如 minisat，“0-depth”和“CNF assignments”的值是什么意思？这些值通常是各种 SAT 求解器信息输出的一部分。
c - SAT 求解超过 2^32 个子句
我正在尝试使用SAT solver. 公式（DIMACS格式）有4,697,898,048 = 2^32 + 402,930,752子句，我能找到的所有 SAT 求解器都遇到了问题：
- (P)lingeling报告“子句太多”（即子句比标题行指定的多，但事实并非如此）
- CryptoMiniSat4 & picosat声称读取标题行时说 402,930,752 个子句太少了 2^32
- Glucose似乎解析了 98,916,961 个子句，然后报告已使用简化将公式求解为 UNSAT，但这不太可能是正确的（公式的初始部分很可能是 SAT）。
有人知道可以处理这么大文件的 SAT 求解器吗？或者是否有类似编译器开关的东西可以回避这种行为？我相信所有求解器都是为64bit linux编译的。（在处理这么大的数字时，我有点菜鸟，抱歉。）
prolog - SAT求解器序言中的基数约束
我必须解决一个SAT问题。该问题有 2 个基数约束，第一个是：每天最多 6 个“同一阶段的班级”，“大学”每天“开放”12 小时，因此您必须生成约束以将它们应用于 SAT 求解器。
第二个基数约束是：每个受试者每周必须至少有 X 小时。
我一直在阅读，第一个最好的方法可能是“排序网络算法”，我不知道第二个虽然我不知道如何实现，甚至都没有开始在 prolog 中实现它。