coprocessor produces empty CNF

[max-waters]

Sometimes the simplified CNF produced by coprocessor is empty. I don't know how to interpret this result.

For example, here's a very simple CNF:

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

Run the command:

./coprocessor -dimacs=preprocessed -enabled_cp3 -ppOnly -rate input

The contents of the file preprocessed is simply:

p cnf 3 0

Is it an error? Or does it imply that input cannot be simplified?

[conp-solutions]

Hi,

a produced empty formula means that Coprocessor was able to show that the formula was satisfiable. With the help of the undo information (see e.g. the scripts/cp.sh script), a model can be constructed.

Best, Norbert

PS: I moved the source here: https://github.com/conp-solutions/riss and will likely remove this repository soonish.

[max-waters]

I see, thanks -- the empty CNF has a single empty model, which is translated back into a model of the original input.

So this means that the undo process is not just a matter of variable substitution. In order to translate a preprocessed model, coprocessor must solve another CNF, right?

[conp-solutions]

An empty CNF might have multiple solutions (depending on the "p cnf" line). The undo information is used to transform the model for the simplified formula back into a model for the original formula. This process is polynomial, basically equivalent to

1. rename the variables back to their original
2. Apply the truth assignment that has been found for the original formula during simplification
3. Satisfy the clauses in the undo.info file, basically by checking whether the clause for being satisfied already, or satisfying the very first literal in the clause

As this stack is constructed such that the above algorithm results in a model of the simplified formula, this procedure is polynomial. Note, two different models for the simplified formula might result in the same for the original one. That heavily depends on the simplification techniques that have been applied. While all techniques preserve satisfiability, some of them do not preserve equivalence (ignoring renaming for simplicity), so the number of models for the simplified and original formula might differ a lot.

[max-waters]

That's interesting. When I run minisat over an empty CNF, it always returns an empty answer v 0. But of course it makes more sense that the empty CNF, say, p cnf 3 0 is actually satisfied by any of the 2^3 combinations of the three literals.

[conp-solutions]

Yeah, that's a problem with MiniSat handling input formulas. It only treats variables it spots in the formula during parsing. I just fixed my MiniSat fork wrt this behaviour:

https://github.com/conp-solutions/minisat

[conp-solutions]

Variables are dropped from the mapping, if they do not occur in the formula any more (except the variables of the whileList file).

A variable is also dropped in case Coprocessor was able to find a unique mapping for a variable (resolved it as unit clause). To keep those variables, another flag has to be set. The following combination worked for me during experiments with a small example formula:

-dense -cp3_keep_set

To be honest, the implementation details of most CNF simplifications are not really documented. There are papers about the technique, but that's about it (sorry for that. Running with the -*-debug options with coprocessor should help a lot).

BTW: please make sure you use the more recent variant of Coprocessor. I fix bugs only in the other repository.

Best, Norbert