All lines must be postfixed with "0"

niklasso / minisat

A minimalistic and high-performance SAT solver

minisat.se

Other

1.01k stars 382 forks source link

All lines must be postfixed with "0" #2

Open jonnybest opened 13 years ago

jonnybest commented 13 years ago

(As mentioned in the mailing list [0])

If this is true, this needs to be mentioned somewhere. I'll type it again: All lines must end in "0". "0" is not a variable.

Google's number one hit on how to deal with minisat [1] does not mention that circumstance. Neither does the readme. Could you please add a hint somewhere? It took me about 3 hours to find out about this. ;_;

[0] https://groups.google.com/group/minisat/msg/e759ddeeb89e65d7 [1] http://www.dwheeler.com/essays/minisat-user-guide.html

niklasso commented 13 years ago

Yes, clauses are separated with 0, not with new-lines. This is how the DIMACS format for SAT problems was specified ages ago. While this is not specific to MiniSat at the very least a link to some DIMACS specification would be in order. I'm leaving this issue up until I've added that somewhere in the documentation.