将顶点总魔术标记问题转化为SAT

Question

我和我的朋友收到了来自title的问题需要解决。

我们发现了简单易用的SAT解算器Cryptominisat。

我们还发现了一篇关于将VTML转换为Sat文章的长文。我们将从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是XX1,1->111

Answer 1

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

2. SAT求解器通常期望变量的编号从1到N，所有在1到N之间(包括1和N(的变量在子句中至少出现一次，而不是用大块未使用的标识符随机编号。解算器可能仍然可以工作，但使用的内存超过了所需的内存。

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

除了这些抱怨之外，您确实有一个SAT实例，当它被提供给SAT解算器时，会产生一个结果。我对顶点全魔术标记一无所知，所以我不能说你是否对实际问题进行了正确的编码。