Iterating in STP to Enumerate All CounterExamples

[Jon Passki]

I'm a newbie to STP and SAT/SMT in general. Knowing that this is #SAT
(thanks @seanhn!), I'm trying to enumerate all counterexamples for a
given SATLIBv1 benchmark. Using the STP commandline and the benchmark
as my input, should I follow the simple process below?

--) Run benchmark through stp, printing counter examples
--) Add a negative constraint against a counterexample provided
--) Re-run benchmark
--) Continue until unsat is returned

Or, is there a more stp way of doing this? Here are my constraints:

--) I'm running this in python, parsing the stp command output,
avoiding native C code. I'm not planning on running the PySTP
bindings, but if that's helpful, I can go there.
--) I'd like to keep the input in SATLIBv1 or v2 format for
portability sake. This is mutable, though.

Also, on the side, what are the "-c" and "-d" flags purposes? I can
read what they're documented as. I just don't see different output
when using or not using the "-p" flag.

TIA!

[Trevor Hansen]

Hi Jon,

If you know in advance that there aren't going to be too many possible
counter-examples then it's not terrible to eliminate them one-by-one.

If you'd like to stick with the SMTLIB language. STP's SMTLIB2 parser
has a partial implementation of the command language, which allows you
to push on extra constriants. STP currently doesn't maintain SAT
solver state between pushes. So you'll probably find it much faster to
use the version of MathSAT submitted to this year's SMTCOMP
application track.

If you have lots of counter examples it's best to output the CNF from
STP and use a specialised #SAT solver. When I last looked the sharpSAT
was the best for the problems I was solving. If you do this you'll
need to use as a minimum: --exit-after-CNF --output-CNF -r --
config_pure-literals=0 . These options could be enough to preserve the
number of counter examples--- but I'm not sure.

> Also, on the side, what are the "-c" and "-d" flags purposes? I can
> read what they're documented as. I just don't see different output
> when using or not using the "-p" flag.

They turn on options that are turned on by default, so in effect don't
do anything.

Welcome to the group,

Trevor.

[Stefan Kölbl]

Hi,

I got follow up question on this.

If you use this workflow (STP -> CNF -> SAT-Solver) what is the best/simplest way to get your solutions back to assignments for bit-vectors. I could not find a documentation in STP on how the bit-vectors correspond to the variables in the CNF to translate the solutions back.

Thanks!