标签: sat

我有一些理论/实际问题,我现在还没有关于如何管理的线索,这里是:

我创建了一个SAT求解器,能够在存在模型时找到模型,并且当使用遗传算法在C中出现CNF问题时,不能证明矛盾.

SAT问题看起来基本上就像这样的问题: 我的目标是使用此求解器在许多不同的NP完成问题中找到解决方案 .基本上,我将不同的问题转换为SAT,用我的求解器解决SAT,然后将解决方案转换为原始问题可接受的解决方案.

我已经成功完成了N*N Sudoku以及N-queens问题,但这是我的新目标:将类调度问题减少到SAT,但我不知道如何形成类调度问题以便轻松转换它在SAT之后.

显然,在几个月内,我们的目标就是制作一张如下图所示的时间表:

我发现这个源代码能够解决类调度但不幸的是没有减少SAT:/

我还发现了一些关于规划的文章(例如http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf).

但是,本文中使用的规划域定义语言似乎对我来说过于笼统,以表示类调度问题.:/

是否有人知道如何有效地形成类调度以便将其减少到SAT以及之后,将SAT解决方案(如果它存在^^)转换为类调度？

我基本上对任何建议持开放态度,我现在不知道如何表示,如何减少问题,如何将SAT解决方案转换为计划......

跟进问题:类调度到布尔可满足性[多项式时间减少]第2部分

我正在使用Python绑定Z3定理证明器(Z3Py).我有N个布尔变量,x1,..,xN.我想表达一个约束条件,即N中的N个应该是真的.我怎么能在Z3Py中做到这一点？有没有内置的支持？我检查了在线文档,但Z3Py文档没有提及任何API.

对于N个中的一个约束,我知道我可以单独表达至少一个是真的(断言Or(x1,..,xN))并且最多只有一个为真(断言Not(And(xi,xj) ))所有i,j).我也知道其他方法来手动表达N-out和N-K-out-of-N约束.但是我的印象是,当解算器内置支持此约束时,它有时比手动表达它更有效.

我正试图用一个解决一个大的CNF公式SAT solver.公式(DIMACS格式)有4,697,898,048 = 2^32 + 402,930,752条款,我找到的所有SAT求解器都有问题:

• (P)lingeling报告"有太多条款"(即比标题行指定的条款更多,但事实并非如此)
• CryptoMiniSat4和picosat宣称读取标题行为402,930,752条款,其中2 ^ 32太少
• 葡萄糖似乎解析了98,916,961条款,然后报告使用简化解决了UNSAT公式,但这不太可能是正确的(公式的初始部分很短很可能是SAT).

是否有人知道可以处理这么大的文件的SAT求解器？或者是否有类似编译器开关的东西可以回避这种行为？我相信所有求解器都是为64位linux编译的.(当谈到处理这么大的数字时,我有点像菜鸟.抱歉.)

我正在开发一个流规则引擎，我的一些客户有几百条规则，他们想对到达系统的每个事件进行评估。规则是纯（即无副作用）布尔表达式，它们可以任意深度嵌套。

客户在运行时创建、更新和删除规则，我需要动态检测和适应规则的数量。目前，表达式计算在内部 AST 上使用解释器，我还没有开始考虑 codegen。

与往常一样，树中的某些谓词的计算成本比其他谓词要便宜得多，而且我一直在寻找一种算法或数据结构，以便更容易找到便宜的谓词，并且可以有效地解释为控制整个表达。我对这种模式的心理标题是“ANDs all way to the root”，即所有祖先都是ANDs的任何谓词都可以解释为控制。

尽管进行了几天的文献搜索，阅读了有关 ROBDD、CNF、DNF 等的信息，但我还是无法从行业中的常见做法到我的特定用例关闭循环。我发现似乎相关的一件事是布尔表达式索引的分析和优化， 但不清楚如何在不自己实现 BE-Tree 数据结构的情况下应用它，因为似乎没有开源实现。

我一直半开玩笑地向我的团队提到，这些天我们将需要一个 SAT 求解器。我想编写一个遍历树并跟踪每个祖先是 AND 还是 OR 的递归算法可能就足够了，但我一直有“这肯定是一个已解决的问题”的感觉。:)

编辑：与几个朋友交谈后，我想我可能有一个解决方案的草图！

1. 将表达式转换为联合范式，根据定义，其中每个节点都处于有效的短路位置。
2. 使用 Tseitin 算法尽量避免 CNF 变换导致的表达式大小的指数膨胀
3. 对于树中的每个AND，按成本升序排序（即最便宜的到左边）
4. ？？？
5. 利润！^Weval 像往常一样:)

我有一个列表Employee和一个列表Mission。每个任务都有开始时间和持续时间。

在CP模型（谷歌CpSat，从或工具包），我定义shifts = Dictionary<(int,int),IntVar>，其中shifts[(missionId, employeeId)] == 1当且仅当这个任务是由这名员工来实现。

我需要将每个任务分配给一名员工，显然一名员工无法同时完成两项任务。我已经写了这两个硬约束，它们运行良好。

问题：

现在，有些任务是“链接”在一起的，应该由同一个员工来实现。它们存储如下：

linkedMissions = {{1,2}, {3,4,5}}

在这里，任务1和任务2必须由同一个员工共同实现，任务3、4和5也是如此。

为了编写这最后一个约束，我为每个员工收集了应该链接在一起的所有班次的列表，然后我让它们都相等。

foreach (var employee in listEmployeesIds)
foreach (var missionGroup in linkedMissionsIds)
{
    var linkedShifts = shifts
        .Where(o => o.Key.Item2 == employee
                    && missionGroup.Contains(o.Key.Item1))
        .Select(o => o.Value)
        .ToList();

    for (var i = 0; i < linkedShifts.Count - 1; i++) 
        model.Add(linkedShifts[i] == linkedShifts[i + 1]);
}

然而，求解器告诉我该模型不可行，但我可以用纸和笔轻松找到工作计划。我有 35 名员工和 25 个任务，连接在一起的任务不重叠，所以应该没有任何问题。

编辑：

作为替代方法，正如@Laurent Perron 所建议的，我尝试对所有必须在一起的班次使用相同的布尔变量：

var constraintBools = new …

我正在尝试编写一种天真寻找布尔公式(NNF,但不是CNF)模型的算法.

我所拥有的代码可以检查一个现有的模型,但是当被要求查找模型时它会失败(或者没有完成),似乎因为它产生了无数的解决方案member(X, Y).[X|_], [_,X|_], [_,_,X|_]...

到目前为止我所拥有的是:

:- op(100, fy, ~).    
:- op(200, xfx, /\).  
:- op(200, xfx, \/).  
:- op(300, xfx, =>).  
:- op(300, xfx, <=>). 

formula(X) :- atom(X).
formula(~X) :- formula(X).
formula(X /\ Y) :- formula(X), formula(Y).
formula(X \/ Y) :- formula(X), formula(Y).
formula(X => Y) :- formula(X), formula(Y).
formula(X <=> Y) :- formula(X), formula(Y).

model(1, _).
model(X, F) :- atom(X), member([X, 1], F).
model(~X, F) :- atom(X), member([X, 0], F). % NNF
model(A /\ B, …

在通过冲突驱动子句学习解决 SAT 问题时，每次求解器检测到一组候选变量分配导致冲突时，它必须查看冲突的原因，从中导出一个子句（即，根据整体问题）并将其添加到已知子句集中。这需要在蕴涵图中选择一个切口，从中导出引理。

执行此操作的常见方法是选择第一个唯一蕴含点。

根据https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-sat/cdcl.html

如果从最新决策文字顶点到冲突顶点的所有路径都经过 l，则蕴涵图中的顶点 l 是唯一蕴含点 (UIP)。

标准术语中的第一个UIP 是从冲突回溯时遇到的第一个 UIP。

用替代术语来说，UIP 是蕴含图上相对于最新决策点和冲突的主导者。因此，可以通过构建蕴含图并使用标准算法来查找支配者来找到它。

但寻找支配者可能会花费大量的 CPU 时间，而且我的印象是实用的 CDCL 求解器使用特定于此上下文的更快算法。然而，我找不到比“获取第一个 UIP”更具体的内容。

查找第一个 UIP 的最著名算法是什么？

最近，我开始研究形式验证技术。在文献中，模型检查器和求解器以某种方式互换使用。但是，模型检查器和求解器是如何相互连接的？

ps 如果建议一些论文或链接，我将不胜感激。

我有兴趣计算一个问题的解决方案数量（不列举解决方案）。为此，我有使用CNF文件的工具。我想转换Minizinc文件（mzn 或 Flatzinc fzn 格式）并将其转换为 CNF。

我了解到Picat能够在加载约束后“转储”CNF 文件。此外，Picat 有一个聪明的模块来解释基本的 Flatzinc 文件。我修改了模块fzn_picat_sat.pi以“转储”CNF 文件。所以，我所做的是使用 mzn2fzn 将 Minizinc 文件转换为 Flatzinc，然后尝试使用我的（稍微）修改过的 fzn_picat_sat.pi版本将其转换为 CNF 。

我想要什么：我希望 Picat 加载 Flatzinc 文件并转储适当的 CNF 文件。如果原来的问题有X个解，我期望对应的CNF有X个解。

会发生什么：我尝试过的大多数 Flatzinc 文件都运行良好。但有些似乎会产生不需要的结果。例如，下面的 mzn转换为这个 Flatzinc 文件。该文件只有 211 个解决方案，但Picat转储的CNF 文件有超过 130k 个解决方案。许多 SAT 求解器可以显示 CNF 文件有超过 211 个解（例如带有选项的cryptominisat--maxsol）。奇怪的是，当我要求 Picat 解决 Flatzinc 文件而不转换为 CNF 时，Picat 确实只找到了 211 个解决方案。问题似乎出在翻译的某个地方。最后，即使 CNF 文件有很多使用 Picat 的解决方案，我也会收到错误 …

我需要找到所有 16 位数字 ( x, y, z) 的三元组（实际上只有在不同三元组中与相同位置的位完美匹配的位），这样

y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787

直接使用 8700K 的策略需要大约 2 天，这太多了（即使我会使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。

如果位移位不在等式中，那么这样做将是微不足道的，但是使用位移位很难做同样的事情（甚至可能是不可能的）。

所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（类似于“x XOR 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用 Prolog 语言之类的语言编写（或只是解释他们使用真值表操作）执行所有明确的位将被发现。这个解决方案也很困难：我不知道如何编写这样的解析器，也没有 Prolog 的经验。(*)

所以问题是：这样做的最佳方法是什么？如果是 (*) 那么怎么做呢？

编辑：为了更容易在此处编码数字的二进制模式：

0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111