SAT: disjunction operator

Previous:

1. getting started
2. langford pairs
3. how not to "negate"

I want to create an operator that turns the disjunction of a set of CNFs, into one CNF. That is to say, for c ... d given, find g such that:

I got no relevant hits on "disjoint" or "disjunction" in the pysat documentation. The implementation of the operator is not very complicated, however.

The idea is to do a Tseytin transformation. For each CNF in the input, we create a variable p that is equivalent to the satisfaction of the CNF. Call this variable an indicator variable. We have:



This relationship can be turned into a CNF (standard AND-constraint):



So the method is: create indicators and indicator clauses for all input CNFs. We add all indicator clauses together into a joint CNF. Lastly, we need to add a clause with all indicators, since we need to make sure that at least one indicator is true. The code:

Now we can test it. Let's see if we can make a CNF that is true if and only if the sum of the variables is even. The code:

I modified enumeration_test so that if outputs which variable sums are present in the satisfying assignments, and in the unsatisfying assignments, respectively. The output is as expected:

Satisfying assignments:
{0, 2, 4, 6, 8, 10}

Unsatisfying assignments:
{1, 3, 5, 7, 9}

In conclusion, we could do disjunction as expected. Note that auxiliary variables were present here (implicit from the "equals" clauses, which use sequential counters), as in the negation experiment. But in this case, it worked fine.