Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

All lines must be postfixed with "0" #2

Open
jonnybest opened this issue Apr 23, 2011 · 1 comment
Open

All lines must be postfixed with "0" #2

jonnybest opened this issue Apr 23, 2011 · 1 comment

Comments

@jonnybest
Copy link

(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
Copy link
Owner

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.

jirislaby pushed a commit to jirislaby/minisat that referenced this issue Nov 4, 2019
Fix linking of minisat as dependency library on MacOSX
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants