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

我有伪布尔问题，我需要用sat4j来解决它。关于sat4j，如何使用sat4j来解决伪布尔问题？

有人可以帮助我吗？

这里是我的问题：

我有一个名为的变量列表：A，B，C，d，E，F
而且我所代表的值的列表：＃ 1，＃2，＃3 .....
H（A，＃1）是指分配＃1到

我有一些实施例C onstraints：

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

来源

2017-08-17 JulieZhu

我不会用CNF解决这个问题。 SMT更合适。 –

什么样的SMT解算器？你能向我推荐一个吗？我需要将代码与我的java项目集成，所以我想要一个解决pudo布尔问题并提供java API的工具。 – JulieZhu

Z3是我用过的一种流行的SMT解算器。我还没有试图用Java来谈论它，但其他人也有，至少据Google说。在任何情况下，Z3的简单LISPy I/O语法都不会很难解析。 –

如果我正确理解你的问题是一个伪布尔满意度的问题，可以直接对其进行编码，作为OPB file：

* #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)为，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 [email protected] 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,,x4,x6和x7为假。

（我敢肯定有办法做到使用org.sat4j.pb Java API同样的事情，但也许这个命令行的食谱给你一个起点，帮助您找出答案。）

来源

2017-11-05 13:44:53

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

回答

相关问题