Cryptominisat - Update Version

[Stefan Kölbl]

Hi All,

I just wanted to know if/how it is possible to run the latest version of Cryptominisat with STP.

I can generate the CNF with STP for cryptominisat but would like to get the output of STP for the solutions. Is there some kind of interface for this I'm missing?

If you have some workaround for this I would be happy to know.

-- Stefan

[Stephen McCamant]

>>>>> "SK" == Stefan Koelbl <koel...@gmail.com> writes:

SK> Hi All,
SK> I just wanted to know if/how it is possible to run the latest
SK> version of Cryptominisat with STP.

SK> I can generate the CNF with STP for cryptominisat but would like
SK> to get the output of STP for the solutions. Is there some kind of
SK> interface for this I'm missing?

SK> If you have some workaround for this I would be happy to know.

I believe that Mate Soos (the primary developer of CMS and also a
contributor to STP) already has some plans for updating STP so that
its internal CryptoMiniSat is the latest one.

Using STP with an external SAT solver is a quite reasonable thing to
try: I've thought about doing it myself in a couple of different
contexts. As you explain in a bit more in your other message, it's
trivial to do this if you just want a SAT/UNSAT answer, but in many
application situations it's also important to get the satisfying
assignment back. As far as I know there's no particular support for
doing that back-translation at the moment, but conceptually it's
straightforward. In testing one small example a while ago I was able
to dump the vector of CNF variables corresponding to each bitvector
variable (patch attached).

Hope this helps,

-- Stephen

[Stefan Kölbl]

Thanks for your reply! I've tried out your patch and it prints out some of the variables. However, a large subset of variables is not printed out.

[Stephen McCamant]

SMcC> In testing one small example a while ago I was able to dump the
SMcC> vector of CNF variables corresponding to each bitvector variable
SMcC> (patch attached).

>>>>> "SK" == Stefan Koelbl <koel...@gmail.com> writes:

SK> Thanks for your reply! I've tried out your patch and it prints out
SK> some of the variables. However, a large subset of variables is not
SK> printed out.

I can't say I'm too surprised; as you could probably tell the patch
was somewhat of a one-off hack. I can speculate about several possible
causes/fixes:

* If your formula involves arrays, STP's solving strategy attempts to
use only an abstraction of the formula, and the naming may also be
more complicated.

* STP attempts to remove unconstrained variables from the formula (and
recent changes have made it even more aggressive, for instance
eliminating unconstrained bit positions). If this is the only thing
that's happening, it might be sufficient to assume that any
variables you don't have a mapping for can be set to 0 (or 1, or
random values).

* You can try disabling optimizations with command-line flags (or, if
that fails, by commenting out code). Of course you might be
unsatisfied if you make it easier to recover variable names but at
the same time make the solving take longer.

If you're having trouble getting to the bottom of what's happening,
creating a small input file that demonstrates the unexpected behavior
might be helpful both for your own understanding and for discussions
with other developers.

Last but not least, I think that writing code to make STP interface
with an external SAT solver would not be too much work (for instance,
see the base class src/sat/SATSolver.h). STP is a volunteer project
that depends on improvements contributed by users, and that could
include you.