0

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?

Clíodhna
  • 818
  • 1
  • 15
  • 29
JulieZhu
  • 1
  • I wouldn't use a CNF solver on this. SMT is a much better fit. – Kyle Jones Aug 17 '17 at 18:08
  • what kind of SMT solver? can you recommend one to me? i need to integrate the code with my java project, so i want a tool that both solve pesudo boolean problem and offers java API. – JulieZhu Aug 18 '17 at 01:36
  • Z3 is a popular SMT solver that I've used recreationally. I haven't tried to use Java to talk to it, but others have, at least according to Google. Z3's simple LISPy I/O syntax won't be hard to parse in any event. – Kyle Jones Aug 18 '17 at 02:08
  • yeah, i know the tool z3, but it doesn't offer java api. – JulieZhu Aug 18 '17 at 03:29
  • Looks like other people have already done the API work. I suspect it will be easier to use Z3 than coding adders and comparison circuits, which is what you'll need to do to use a CNF-based solver. – Kyle Jones Aug 18 '17 at 03:32
  • @KyleJones A pseudo-boolean solver like `org.sat4j.pb` doesn’t require manually built adders and comparators to express these constraints. – Anders Kaseorg Nov 05 '17 at 14:06

1 Answers1

0

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.)

Anders Kaseorg
  • 3,657
  • 22
  • 35