Given a set of binary strings, all of length $s$, is it possible to construct a SAT instance with s literals that is satisfied only by those binary strings as assignments?

For example, consider the set $\{101, 110\}$. Can we construct a SAT instance with literals $x_1$, $x_2$, and $x_3$ such that it is satisfied only by the assignments $x_1 = 1$, $x_2 = 0$, $x_3 = 1$ or $x_1 = 1$, $x_2 = 1$, $x_3 = 0$?

It would be even more useful if this instance is an instance of k-SAT for some k.

  • $\begingroup$ I notice I seem to be getting downvotes. Apologies if this is not considered research-level, I am not especially familiar with this field and this pertains to a research problem I am working on. $\endgroup$ – Rohil Prasad Jan 26 '14 at 0:38
  • 1
    $\begingroup$ Each $k$-CNF clause removes exactly one $k$-bit assignment. The example you give has six $3$-bit assignments that must be removed: $000, 001, 010, 011, 100,$ and $111$. For example, $(\neg x1 \lor \neg x2 \lor \neg x3)$ removes $111$. $\endgroup$ – Russell Easterly Jan 26 '14 at 4:18

Every such set of strings determines a collection of rows in the truth table, and so you want an expression that is logically equivalent to the disjunction of those rows. This gives a logical expression in disjunctive normal form, but every propositional assertion can be put into conjunctive normal form, which makes it an instance of SAT.

  • $\begingroup$ Note that converting propositional assertions into conjunctive normal form, however, is quite computationally difficult: if we just want to preserve satisfiability, it's already $NP$-hard, and if we want to actually get an equivalent proposition in CNF then the only upper bound I know is $EXPTIME$ (although that's probably massive overkill). $\endgroup$ – Noah Schweber Jan 26 '14 at 0:46
  • $\begingroup$ Well, he wanted an expression that had exactly those satisfying instances, so one seems to need an expression that is exactly equivalent to the one I am talking about. But I agree that there is exponential cost in doing the conversion---and not only is there a cost for converting, but the resulting CNF expression can become exponentially longer than the original set. $\endgroup$ – Joel David Hamkins Jan 26 '14 at 0:55
  • $\begingroup$ I believe if additional variables are allowed there is polynomial 4-CNF encoding. $\endgroup$ – joro Jan 26 '14 at 7:09

I suppose by "literals" you mean variables.

If you allow additional temporary variables there is explicit polynomial encoding in 4-SAT by carefully constructing the CNF.

First we construct CNFs for the satisfying assignments, then do disjunction of the CNFs.

Encode binary string $s$ this way. For the $i$-th digit introduce boolean variable $v_i$. $1$ is $v_i$, $0$ is $\lnot v_i$.

A satisfying assignment is conjunction $ v_1' \land v_2'\ \cdots \land v_n'$ where $v_i'$ is either $v_i$ or $\lnot v_i$.

To encode the conjunction, use AND gate in CNF encoding.

The CNF for $ AND(A,B,C) := C \iff (A \land B$) is $$ \begin{aligned} & \lnot A \lor \lnot B \lor C \\ & A \lor \lnot C \\ & B \lor \lnot C \end{aligned} $$

By using the AND gate and fresh variables $w_i$, encode each satisfying assignment $s_i$ to a 3-CNF $C_i$.

Basically $C_i = \{AND(v_1',v_2',w_1), \ldots AND(v_k',w_{k-1},w_k), w_n \}$

Remains to encode the disjunction of the CNFs $C_i$.

Define the transformation $F(C_i)$ by introducing boolean variable $y_i$ and add $\lor y_i$ to each clause of $C_i$ (this is just adding $y_i$ to the CNF clause).

If $y_i$ is $False$, then $F(C_i)$ is just $C_i$ and it is satisfiable only by $s_i$.

To force at least one $y_i$ to be $False$ add the clause $$ \lnot y_1 \lor \lnot y_2 \cdots \lor \lnot y_n$$.

So the final CNF is $CN = \{F(C_1) \ldots F(C_n), \lnot y_1 \lor \lnot y_2 \cdots \lor \lnot y_n\}$.

which by construction is 4-SAT and is polynomial in the size of the input.

Using an AND gate adds 3 clauses and one new variable and this is polynomial.

  • $\begingroup$ Why not just go directly to 3CNF? Make a Boolean circuit with two inputs per gate that implements the obvious DNF formula for the given set of truth assignments and then make extra variables for the internal states on each wire of the circuit and clauses for the consistency of each gate. $\endgroup$ – David Eppstein Jan 26 '14 at 8:31
  • $\begingroup$ Well, it is not 4-CNF because of the last clause. Another approach for disjunction is just to OR the outputs of the CNFs in a single clause. $\endgroup$ – joro Jan 26 '14 at 13:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.