关于sat4j，如何使用sat4j解决伪布尔问题？

Question

我有伪布尔问题，我需要用sat4j来解决它。

有人能帮我吗？

我的问题是：

• 我有一个名为a，b，c，d，e，f的变量列表。
• 我有一个值列表表示：#1，#2，#3.
• h(a，1)是指将#1分配给

我有一些限制因素：

h(a,#1)=1
h(a,#1)+h(b,#1)+h(c,#1)=1
h(a,#1)+h(a,#5)>=1
h(b,#2)+h(b,#3)+h(b,#4)>=1

如此多的约束，如上面的例子。最后，我想要分配哪个值给哪个值的结果。

如何用sat4J来解决这个问题？我应该如何表示约束？

Answer 1

如果我正确地将您的问题理解为伪布尔满意问题，则可以将其直接编码为OPB文件。

* #variable= 7 #constraint= 4
1 x1 = 1;
1 x1 1 x2 1 x3 = 1;
1 x1 1 x4 >= 1;
1 x5 1 x6 1 x7 >= 1;

其中我任意地将h(a,#1)编码为x1，h(b,#1)为x2，h(c,#1)为x3，h(a,#5)为x4，h(b,#2)为x5，h(b,#3)为x6，以及h(b,#4)为x7。(您可能希望添加如下的约束

-1 x1 -1 x4 >= -1;
-1 x2 -1 x5 -1 x6 -1 x7 >= -1;

说明每个变量最多有一个值，或者=只包含一个值。)

那就跑

java -jar org.sat4j.pb.jar yourfile.opb

它的输出(忽略以c开头的许多注释行)：

s SATISFIA@KyleJones You don’t need to manually build adders and comparators to use a pseudo-boolean solver like `org.sat4j.pb`.BLE
v x1 -x2 -x3 -x4 x5 -x6 -x7 

意思是x1和x5是真，而x2、x3、x4、x6和x7是假的。

(我确信有一种方法可以使用Java来做同样的事情，但也许这个命令行的菜谱为您提供了一个起点来帮助您解决这个问题。)