search

msoos / cryptominisat

An advanced SAT solver
https://www.msoos.org
Other
814 stars 178 forks source link

CMS 3.x: Line breaks in clauses - valid or not? #140

Closed capiman closed 10 years ago

capiman commented 10 years ago

I have used CMBC (C Bounded Model Checker) (see http://www.cprover.org/cbmc )

-33 -98 0 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 98 0 99 100 0

There the second clause has line breaks. I reported this to developer of CBMC and he told me, some SAT solver have problems with long lines and line breaks in clauses are valid in CNF.

Can you confirm this? Bug in CMS? Or not really defined?

capiman commented 10 years ago

BTW: cbmc can export internal used CNF via "--dimacs --outfile mm.cnf" (usually internal MiniSat is used)

Example: cbmc mm.c --function myfunction --bounds-check --dimacs --outfile mm.cnf

msoos commented 10 years ago

This is simply wrong. Lines breaks are not acceptable. Here is the definition:

http://www.satcompetition.org/2009/format-benchmarks2009.html

Cheers,

mate