search

nmanthey / riss-solver

sequential and parallel SAT solver
GNU Lesser General Public License v2.1
8 stars 3 forks source link

-dense produces invalid output #15

Closed max-waters closed 6 years ago

max-waters commented 6 years ago

I have found that using the -dense flag with Coprocessor produces an invalid CNF. The problem is that a model of the preprocessed CNF, when translated back using the undo info, is not a valid model of the original CNF.

I have attached a small script to demonstrate the problem (undo-test.zip). It can be run with, for example, ./undo-test.sh example.cnf 10.

This hasn't been tested against the latest version of riss, as I haven't been able to get it to build. But, before I spend ages trying to compile the latest version, could you confirm whether or not this is a bug, and if so whether it exists in the latest version?

max-waters commented 6 years ago

Never mind! Fixed in the latest version.