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