Constructing 2-SAT Constraints for Exactly Three Assignments

We are given $n$ Boolean variables $x_1, x_2, \cdots, x_n$ that can take values $0$ (false) or $1$ (true). A 2-SAT constraint is a logical implication of the form $a\to b$, where both $a$ and $b$ are literals (either $x_i$ or its negation $!x_i$). Recall that $a\to b$ is logically equivalent to $\lnot a\lor b$, and the constraint is satisfied if this clause evaluates to true.

You are given three distinct assignments (each a sequence of $n$ bits) that satisfy some unknown 2‐SAT formula. It is known that these three assignments are the only assignments satisfying that formula. Your task is to output any list of at most 500 2‐SAT constraints that have exactly these three assignments as their solutions.

A valid output consists of an integer $m$ (the number of constraints), followed by $m$ lines. Each line describes a constraint of the form

a -> b

where a and b are literals. In our notation a literal is either xk (meaning $x_k$ is true) or !xk (meaning $x_k$ is false), with indices starting at 1.

One way to solve this problem is to eliminate every assignment that is not one of the three given ones. Notice there are $2^n-3$ unwanted assignments. For each unwanted assignment $U$, one can find a clause of two literals (written in implication form) that is satisfied by all three given assignments and falsified by $U$. More precisely, for some pair of distinct indices $i,j$ and a choice of literals $L_i$ and $L_j$ (where $L_i$ is either x_i or !x_i and similarly for $L_j$), the clause

(L_i or L_j)  (*),

which can be written in implication form as

(not L_i) -> L_j

is chosen so that for every allowed assignment $D$, at least one of $L_i$ or $L_j$ evaluates to true, but for the unwanted assignment $U$ both evaluate to false. If one does this for every unwanted assignment, then the only assignments that satisfy all the constraints will be exactly the three given ones. (It can be shown that when $n$ is small enough – and indeed the restriction $m\le500$ forces $n$ to be relatively small – such pairs exist.)

Your program should read the three assignments and output a valid list of constraints constructed in this way. The answer may be any correct list of at most 500 valid constraints.

inputFormat

The first line contains an integer $n$ ($2\le n\le 8$). The next three lines each contain $n$ space-separated integers (either 0 or 1), representing the three distinct assignments that satisfy the (hidden) 2-SAT formula.

outputFormat

First, output an integer $m$ indicating the number of constraints. Then output $m$ lines, each line containing a constraint in the form a -> b where a and b are literals. The generated list of constraints must be such that its only solutions (assignments satisfying all constraints) are exactly the three given assignments.

sample

2
0 0
0 1
1 0

1
x1 -> !x2

</p>