Is there a 2SAT encoding for a NAND gate

Question

I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?

Answer 1

It seems, based on the comments in other answers, that what you are after is a 2-CNF formula $\phi(q, a, b)$ equivalent to $q \iff \overline{a \land b}$. This is indeed not possible; the only possible clauses in $\phi$ are of the form $(\ell_1 \lor \ell_2)$, with $\ell_1, \ell_2 \in \{a, \bar{a}, b, \bar{b}, q, \bar{q}\}$, and thus there are at most $36$ possible clauses. Given that adding a clause more than once does not change the truth table of a formula, all possible 2-CNF formulas over variables $a, b, q$ are completely defined by a subset of the at most $36$ possible different clauses, and you can check by a program that the desired truth table is not achieved by any of the possible subsets.

Below my Python code:

import itertools
import more_itertools

lts = ['a', 'b', 'q', '~a', '~b', '~q']

potential_clauses = []
for i in range(len(lts)):
    for j in range(i, len(lts)):
        potential_clauses.append((i, j))


def target(a, b, q):
    return q != (a and b)


def eval_clause(valuation, clause):
    lits = []
    for var in 'abq':
        if valuation[var]:
            lits.append(var)
        else:
            lits.append('~' + var)

    for lit in clause:
        if lit in lits:
            return True
    return False


def eval_clauses(valuation, clauses):
    for clause in clauses:
        if not eval_clause(valuation, clause):
            return False
    return True

for clauses in more_itertools.powerset(potential_clauses):
    works = True
    for prod in itertools.product([0, 1], repeat=3):
        a, b, q = prod
        valuation = { 'a' : a, 'b': b, 'q': q}
        if target(a, b, q) != eval_clauses(valuation, clauses):
            works = False
            break
    if works:
        print("Found it! " + clauses)

Answer 2

There is no proof that it is impossible, but it is believed that it's unlikely to be possible, because if you could convert every circuit with NAND gates to 2CNF, you would have a proof that P = NP. (This is because there are known polynomial-time algorithms to test the satisfiability of 2CNF; if such a conversion existed, then by the universality of NAND gates, this conversion would give a polynomial-time way to test the satisfiability of arbitrary boolean circuits, and the latter is known to be NP-complete.)

Answer 3

If you could encode Q = A NAND B using a conjunction of disjunctive clauses with 2 literals, then you could transform any circuit into a polynomial-size 2-SAT formula (NAND gates are universal). This would allow to check whether there is a set of inputs for which the circuit outputs "true" in polynomial-time.

However this problem is known to be NP-Complete.