CNF file not created

[Linus F.]

Hi,

can anyone help me with my problem I just posted on the stp github site:

https://github.com/stp/stp/issues/104

Thanks,
Linus

[Stephen McCamant]

>>>>> "LF" == Linus F <fei...@informatik.uni-freiburg.de> writes:

LF> Hi,
LF> can anyone help me with my problem I just posted on the stp github site:

LF> https://github.com/stp/stp/issues/104
LF> [Summary: STP is solving my input file without producing CNF, but
LF> I want a CNF form of my file to use with a #SAT solver]

I'll cross-post my reply here, though if we continue the discussion we
should probably choose one forum or the other.

I think your diagnosis that STP is managing to solve the formula
during pre-processing is correct. The "-s" option is useful for
getting an overview of the progress of simplification. Even with
"--disable-simplify -w -a --disable-cbitp --disable-equality", the
first few lines I see are:

[2ms:25MB]input asserts and query: Node size is: 8
Difficulty Initially:50
Array Sizes:
Have removed array operations
[0ms:25MB]After Removing Unconstrained. Node size is: 1

By the time the size is 1 I think it's safe to say not much of the
formula is left, though it gets down to 0 later.

What you're hoping for STP to do is not one of its standard use cases:
STP's design is to use the SAT solver only as needed. (A related issue
which came up briefly on the mailing list recently is that STP also
doesn't provide a standard way to map between the CNF variables and
the SMT variables.) So it doesn't look to me like there's a clean fix
for this that doesn't involve changing the STP implementation
somehow. If you're willing to do something that's more of a hack, you
could try coming up with "weird, unsimplifiable" constraints to
partition your original problem into sub-problems which all make it to
CNF (and then sum up the counts), though it seems tricky to be sure
you're always breaking the simplifier.

Since the problem seems to mostly be simplification that you do not
want to happen, it might be fixable by just disabling more
simplifications. The flag --disable-simplify is documented as "disable
all simplifications", so arguably it's a bug that things like removing
unconstrained variables are still happening with it set.

Depending on the broader context in which you're doing this, you might
want to check out the QEST'13 paper on "SAT-Based Analysis and
Quantification of Information Flow in Programs" if you're not already
familiar with it, which does something similar. They use CBMC to go
straight from C to CNF without stopping at SMT. If you already have
SMT, going QF_BV -> C -> CNF sounds a bit backwards but could probably
be made to work.

Hope this helps,

-- Stephen

[Linus F.]

Thanks for the reply. I answered in the other github forum.
Or which of the forums would you recommend for further discussion?
Would be happy to take your advise, as I am new here.
Thanks, Linus