views:

3

answers:

0

Hello,

So I downloaded the latest version of zChaff (2007), and was trying out some very simple SAT problems. But zChaff does not output the solution (variable assignments). A very simple example input:

p cnf 2 2
1 2 0
1 -2 0

And what I get:

c 2 Clauses are true, Verify Solution successful.
Instance Satisfiable
1 -2 Random Seed Used    0
Max Decision Level    1
Num. of Decisions    2
( Stack + Vsids + Shrinking Decisions )  0 + 1 + 0
Original Num Variables    2
Original Num Clauses    2
Original Num Literals    4
Added Conflict Clauses    0
Num of Shrinkings    0
Deleted Conflict Clauses   0
Deleted Clauses     0
Added Conflict Literals    0
Deleted (Total) Literals   0
Number of Implication    2
Total Run Time     5.1e-05
RESULT: SAT

I can see the 1 -2 on the left of "Random Seed Used", but shouldn't this be outputing the variable assignments as "v ..." ?

Thanks