About sat4j, how to use sat4j to solve pseudo boolean problems?

Question

I have pseudo boolean problems and I need to solve it with sat4j.

Can someone help me?

Here's my problem:

• I have a list of variables named: a,b,c,d,e,f

• And I have a list of values represented by: #1, #2, #3.....

• h(a,#1) means assign #1 to a

I have some example constraints:

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

So many constraints like examples above. Finally, I want a result of assign which values to which value.

How can I solve it with sat4J? How should I represent the constraints?

Answer 1

If I understand your problem correctly as a pseudo-boolean satisfaction problem, you can directly encode it as an 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;

where I have arbitrarily encoded h(a,#1) as x1, h(b,#1) as x2, h(c,#1) as x3, h(a,#5) as x4, h(b,#2) as x5, h(b,#3) as x6, and h(b,#4) as x7. (You may wish to add constraints like

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

stating that each variable has at most one value, or = for exactly one value.)

Then run

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

which outputs (ignoring many comment lines beginning with 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 

meaning x1 and x5 are true while x2, x3, x4, x6, and x7 are false.

(I’m sure there’s a way to do the same thing using the org.sat4j.pb Java API, but perhaps this command-line recipe gives you a starting point to help you figure that out.)