Minor logic errors in simplification

[chanseokoh]

This was reported a long time ago, but no action has been taken since then. To make it conspicuous, and as a record, I am opening an issue.

Details can be found here:
https://groups.google.com/forum/#!searchin/minisat/chanseok/minisat/ldiQ82kdLzA/2NzpebK7qEkJ

[johntyree]

Still no action on this. I was hoping to play with the simplifier but it's outputting clearly wrong reformulations, e.g.

$ ./minisat -no-solve -dimacs=simplified <<EOF                                                       
p cnf 2 1
1 2 0
EOF

$ cat simplified
p cnf 0 0

I would disable this entirely until it's looked at. Wrong is worse than absent.

[chanseokoh]

It's generating the right output. The above CNF formula is quite trivially satisfiable. In this case, you get an empty theory after simplification, which means the formula is vacuously true. This interpretation of an empty theory is a logically- and mathematically-established interpretation. Informally speaking, there is no constraint to satisfy.

The bugs reported in the Google Group do not affect the correctness. It is merely a performance issue, if it affects performance at all. Moreover, you don't even hit the bug because you're using the default simplification parameters in your example above.

Lastly, as pointed out later by Fahiem in the Google Group thread, the second bug I reported was not a bug.

[johntyree]

@chanseokoh I'm new to this so perhaps I am misunderstanding something. The single clause above can be translated to "either x1 or x2 must be true." The solution is empty, suggesting that any assignments of anything will do just fine.

What about my interpretation is incorrect?

[chanseokoh]

@johntyree The misunderstanding here arises from the fact that your command

$ ./minisat -no-solve -dimacs=simplified <<EOF

does not return a solution but rather discharges a simplified formula in DIMACS (i.e., in CNF that you can feed again into any SAT solver). The header of the output 'p cnf 0 0' clearly shows that the output is a CNF formula in DIMACS. If you want to get a solution, remove the two parameters: -no-solve and -dimacs.

[TomMD]

@johntyree Can I take a stab at re-stating the problem?

If the original problem is orig(env) = env.x1 OR env.x2 (orig is a function that takes an environment and returns a Boolean) and you assert that another function is constructed from the original via new = minsat -notsolve -dimacs=simplified orig.cnf then it should be the case that:

forall env . orig(env) = new(env)

However, if env.x1 = env.x2 = False then orig(env) = False but new(env) = True. This contradicts the above requirement and you interpret it to be a bug.

On the other hand, from the perspective of a satisfiability solver we don't actually care about the predicate above. What we care about is sat(orig) = sat(new). Since they are both satisfiable, perhaps under different assignments, the transformation is in some sense valid.

[chanseokoh]

@johntyree After reading what @TomMD said, I think now I get what you were asking. Sorry!

Adding to what @TomMD said, the resulting formula after simplification is not logically equivalent to the original formula, chiefly because the two formulas do not have the same number of variables. In other words, this logical inequivalence happens whenever a variable is eliminated by simplification, which almost all the time happens in practice. However, note that the simplified formula preserves satisfiability. That is, it is equi-satisfiable to the original formula.

If you want to manually reconstruct a correct solution for an original formula after solving a simplified formula that is not equivalent but equi-satisfiable to the original one, you need to do some extra work (which is not so difficult if you book-keep necessary information) to extend a solution to the simplified formula so that it works correctly on the missing variables. Solvers that perform preprocessing take care of this extra work automatically.

[johntyree]

Aha! I did not realize that that's what it was doing, thank you.

Can you explain why it wouldn't just output an empty DIMACS file for all satisfiable problems, then?

[chanseokoh]

I anticipate that MiniSat would output an empty DIMACS file if the preprocessing step alone was enough to solve the problem and figure out that an input formula is satisfiable. I skimmed over the MiniSat code, and I think it is indeed the case. If not, then there is no particular reason for not doing so.

[johntyree]

@chanseokoh OK that makes sense now that I understand that the preprocessing step is not trying to find a model, but simply find another problem with the same satisfiability.

Do you know of any particular research done towards simplifying a problem while maintaining that forall env . orig(env) = new(env), as @TomMD put it?

For example,

p cnf 3 3
1 2 0
-2 3 0
1 3 0

might reduce to

p cnf 2 2
1 2 0
-2 3 0

[TomMD]

@johntyree You could run a SAT solver that gives you a set of assignments plus an unsat core. Then to construct the equivalent problem you re-produce the unsat core and add the assignments in as new CNF clauses with a single, possibly negated, literal.

[johntyree]

@TomMD yes that would be optimal. It doesn't really help me do what I hoped, which is to do that part faster via heuristics :).

I think I'll lay this to rest for now. When it comes to communicating domain specific problems to the user, I'll give this some more thought.

Thanks, both of you!