Starting a Sat Solver

[Jochen]

Hello

First let me say that I a new to programming with constraints.

My final goal is to find (all) possible solutions to a list of boolean equations.
Right now I already fail at writing the simplest programm. For starterst I just want to find all possible solutions to

a=>b
b=>c

So I wrote :

Store store = new Store();
SatTranslation sat = new SatTranslation(store);
sat.impose();
BooleanVar a = new BooleanVar(store, "a");
BooleanVar b = new BooleanVar(store, "b");
BooleanVar c = new BooleanVar(store, "c");

sat.generate_implication(a, b);
sat.generate_implication(b, c);

The documentation tells me : " The search for solutions is identical with CP framework" .
Can anyone point me to an example or explain me how this is done. Because what I have tried didnt give me any results that look like a solution to the equations above.

Thanks in advance.

Jochen

[kris]

Hi Jochen!

Here is a simple search that generates all solutions to your constraints.

Store store = new Store(); 
SatTranslation sat = new SatTranslation(store); 
sat.impose(); 
BooleanVar a = new BooleanVar(store, "a"); 
BooleanVar b = new BooleanVar(store, "b"); 
BooleanVar c = new BooleanVar(store, "c");

sat.generate_implication(a, b); 
sat.generate_implication(b, c);

BooleanVar[] vars = {a,b,c};

Search<IntVar> label = new DepthFirstSearch<IntVar>();

SelectChoicePoint <IntVar> select = new SimpleSelect<IntVar>(vars, null,
                             new IndomainMin<IntVar>());
label.setSolutionListener(new PrintOutListener<IntVar>()); 
label.getSolutionListener().searchAll(true);

boolean result = label.labeling(store, select);

if (result) {
  System.out.println("Yes");

} else {
  System.out.println("No solution.");
}

The print-out is as follows.

Solution : [a=0, b=0, c=0]

No of solutions : 2
Last Solution : [a=0, b=0, c=1]

No of solutions : 3
Last Solution : [a=0, b=1, c=1]

No of solutions : 4
Last Solution : [a=1, b=1, c=1]

Depth First Search DFS0
[a=1, b=1, c=1]

No of solutions : 4
Last Solution : [a=1, b=1, c=1]
Nodes : 3
Decisions : 3
Wrong Decisions : 0
Backtracks : 3
Max Depth : 3

Yes

Good luck with your experiments,
/Kris

[A. M. Grubb]

Hi Kris (or anyone),

Is there a way to print out constraints imposed in the SatTranslation?

In the previous example you generated two implications:
sat.generate_implication(a, b);
sat.generate_implication(b, c);
can I print these later to show what the solver will solve.

With CSP I got around this by adding all my constraints to the store all at once and printing them before I added them (as follows):
for (int i = 0; i < constraints.size(); i++) {
System.out.println(constraints.get(i).toString());
store.impose(constraints.get(i));
if(!store.consistency()) {
System.out.println("Constraint: " + constraints.get(i).toString());
System.out.println("have conflicting constraints, not solvable");
}
}

Also, what is the relationship, if any, between SatTranslation and SatWrapper?

Thanks in advance,

Alicia

[Jochen]

Thank you very much. Works great.

[kris]

Hi!

No, there is no way currently to print-out generated clauses to SAT solver.

The generation changes your predicate into logical clause or several clauses and store in the SAT solver as single constraint from solver point of view. We did not implemented a method that prints this clauses.

Sorry!
/Kris

[A. M. Grubb]

Did you implement a way to print out the single clause (presumably in CNF)?
Thanks,
Alicia

[kris]

I just checked the code and you can try to do the following.

sat.debug = true;

This should open print-out of generated clauses. Unfortunately it is not in CNF form. It will print you 'positive' and 'negative' variables in a clause (one per line), i.e., not negated and negated in the disjunction (clause).

/Kris

[A. M. Grubb]

"sat.debug = true;" should be sufficient for now. :)
Thanks!
Alicia