python - 将顶点总魔术标签问题转换为 SAT

Question

我和我的朋友从标题收到问题来解决。

我们发现了很好用的 SAT Solver Cryptominisat。

我们还发现了一篇关于将 VTML 转换为 Sat Article的长文章。我们将从 python 生成规则/限制。

我们实际上发现了将整个图转换为布尔规则的障碍。我们也

c 2 na poczatku to jest Y
c 1 na początku to jest X
p cnf 188 5
c i = 1
-111 21 0
111 -21 0
c i = 2
22 -112 0
22 -21 0
-22 112 21 0
c i = 3
23 -113 0
23 -22 0
-23 113 22 0
c i = 4
24 -114 0
24 -23 0
-24 114 23 0
c i = 5
25 -115 0
25 -24 0
-25 115 24 0
c i = 6
26 -116 0
26 -25 0
-26 116 25 0
c jezeli jedno jest true to reszta nie
-21 112 0
-22 113 0
-23 114 0
-24 115 0
-25 116 0
26 0

根据文章，我手动编写了 cnf 子句。2开头是Y，

1 是 X X1,1 -> 111

Answer 1

1. 当只有 12 个活动变量和 23 个子句时，p行声明了 188 个变量和 5 个子句。

2. SAT 求解器通常期望变量从 1 到 N 编号，所有介于 1 和 N 之间的变量在一个子句中至少出现一次，而不是用大块未使用的标识符随机编号。求解器可能无论如何都可以工作，但使用的内存比必要的多。

3. 注释不应出现在p行之后。

除了那些抱怨之外，你确实有一个 SAT 实例，当它输入 SAT 求解器时会产生结果。我对顶点总魔法标签一无所知，所以我不能说你是否正确编码了实际问题。