0

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

有人能帮我吗？

这是我的问题：

  • 我有一个名为：a,b,c,d,e,f 的变量列表

  • 我有一个由以下表示的值列表：#1、#2、#3 .....

  • h(a,#1) 表示将 #1 分配给 a

我有一些示例约束：

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 解决它？我应该如何表示约束？

4

1 回答 1

0

如果我将您的问题正确理解为伪布尔满意度问题，您可以直接将其编码为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)as x2、h(c,#1)as x3、h(a,#5)as x4、h(b,#2)as x5、h(b,#3)asx6和h(b,#4)as 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为假。

（我确信有一种方法可以使用org.sat4j.pbJava API来做同样的事情，但也许这个命令行配方为您提供了一个起点来帮助您解决这个问题。）

于 2017-11-05T13:44:53.033 回答