SAT: How "negate" doesn't work

Previous:

1. getting started
2. langford pairs

I want to explore the python-sat module. One thing that seems simple yet useful is to negate formulas. That is, to create a formula that has the opposite boolean value to a given formula. Let's start with a formula:

This bound was created using a sequential counter explained in [1] (p.8) and defined in [2]. It introduces two auxiliary variables; 4 and 5. We can enumerate all assignments to X and see that the formula works as expected:

Satisfying assignments:
(0, 0, 0)
(0, 0, 1)
(0, 1, 0)
(1, 0, 0)

Unsatisfying assignments:
(0, 1, 1)
(1, 0, 1)
(1, 1, 0)
(1, 1, 1)

Now we can use pysat.formula.CNF.negate to negate this formula. Expected output:

Satisfying assignments:
(0, 1, 1)
(1, 0, 1)
(1, 1, 0)
(1, 1, 1)

Unsatisfying assignments:
(0, 0, 0)
(0, 0, 1)
(0, 1, 0)
(1, 0, 0)

But, using this:

We get:
Satisfying assignments:
(0, 0, 0)
(0, 0, 1)
(0, 1, 0)
(0, 1, 1)
(1, 0, 0)
(1, 0, 1)
(1, 1, 0)
(1, 1, 1)

Unsatisfying assignments:
[]

What happened here?

Explanation

The problem has to do with the auxiliary variables. The problem is that in the original formula (bound_X), there are assignments where the main variables (X)  fulfill the bound, but the assignment of the auxiliary variables (4, 5) make the formula false. By definition, such an assignment will make the negated formula (bound_X_neg) true. Thus, the negated formula can be satisfied even when the main variables are satisfy the original formula.

In conclusion, negating a formula's function with respect to a strict subset of the variables does not work in the general case.

P.S. We see the problem when we iterate over all assignments to X + the auxiliary variables (satisfying assignments for atmost(X, bound=1)):

Satisfying assignments:
X             auxilliary
(0, 0, 0,    0, 0)
(0, 0, 0,    0, 1)
(0, 0, 0,    1, 1)
(0, 0, 1,    0, 0)
(0, 1, 0,    0, 1)
(1, 0, 0,    1, 1)

Unsatisfying assignments:
X             auxilliary
(0, 0, 0,    1, 0)
(0, 0, 1,    0, 1)
(0, 0, 1,    1, 0)
(0, 0, 1,    1, 1)
(0, 1, 0,    0, 0)
(0, 1, 0,    1, 0)
(0, 1, 0,    1, 1)
(0, 1, 1,    0, 0)
(0, 1, 1,    0, 1)
(0, 1, 1,    1, 0)
(0, 1, 1,    1, 1)
(1, 0, 0,    0, 0)
(1, 0, 0,    0, 1)
(1, 0, 0,    1, 0)
(1, 0, 1,    0, 0)
(1, 0, 1,    0, 1)
(1, 0, 1,    1, 0)
(1, 0, 1,    1, 1)
(1, 1, 0,    0, 0)
(1, 1, 0,    0, 1)
(1, 1, 0,    1, 0)
(1, 1, 0,    1, 1)
(1, 1, 1,    0, 0)
(1, 1, 1,    0, 1)
(1, 1, 1,    1, 0)
(1, 1, 1,    1, 1)

[1] Knuth, Donald E. The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability. Addison-Wesley Professional, 2015.

[2] Sinz, Carsten. "Towards an optimal CNF encoding of boolean cardinality constraints." International conference on principles and practice of constraint programming. Springer, Berlin, Heidelberg, 2005.