0
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ I can't understand your attempted revision to the question. Please don't replace the question with something entirely different. Please don't use edits as a way to respond to the answers you have received. Thank you. $\endgroup$
    – D.W.
    Commented Sep 7, 2023 at 20:21

3 Answers 3

2
$\begingroup$

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)
$\endgroup$
5
  • 2
    $\begingroup$ This doesn't account for the possibility of adding auxiliary variables, which I think is a natural thing to allow. But Yuval Filmus' answer to this question shows that adding such variables doesn't help. Also, the answer by David Eppstein gives a more efficient algorithm to test if some truth table corresponds to that of a 2-SAT problem. $\endgroup$
    – Tassle
    Commented Sep 8, 2023 at 11:48
  • $\begingroup$ That’s why I made explicit that I’m talking about equivalence, which requires by definition the same set of variables. Equisatisfiable is a completely different thing (albeit they match in this case as you point out). With respect to algorithms, yes in this particular case there’s also a simple but tedious case analysis (about 8 cases) that works, but given the question is about a concrete instance rather than general expressiveness of 2-CNF, I think any argument that works can do… $\endgroup$ Commented Sep 8, 2023 at 16:13
  • $\begingroup$ You’re free to add an answer using the median property — in fact that would be cool and more elegant! The only downside is that it requires understanding the proof of said property, as opposed to this arguably uglier approach I proposed, whose benefit is being really easy to verify $\endgroup$ Commented Sep 8, 2023 at 16:19
  • 1
    $\begingroup$ No I'm not talking about equisatisfiability, and neither are the two answers I mentioned (transforming to an equisatisfiable 2-SAT problem is trivial and uninteresting: the formula is satisfiable, so just take any satisfiable 2-SAT problem). It is about solely about equivalence (in the case of allowing for more variables, it is about finding a 2-SAT problem whose projection on the first 3 variables is equivalent). I'll maybe add an answer if I get the time (upvoted yours btw, I'm just pointing stuff out). $\endgroup$
    – Tassle
    Commented Sep 8, 2023 at 16:59
  • $\begingroup$ you're right, equisatisfiability is indeed the wrong concept -- I meant the projection equivalence you're mentioning $\endgroup$ Commented Sep 8, 2023 at 17:56
1
$\begingroup$

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.)

$\endgroup$
0
$\begingroup$

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.

$\endgroup$
9
  • $\begingroup$ This doesn't represent the NAND circuit. This represents only the situation where the NAND circuit has Q = 1. This is incomplete. $\endgroup$ Commented Sep 6, 2023 at 23:17
  • $\begingroup$ Please define what Q is and what you mean be "repsesent the NAND circuit". $\endgroup$
    – Steven
    Commented Sep 6, 2023 at 23:18
  • 1
    $\begingroup$ 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. $\endgroup$
    – Steven
    Commented Sep 6, 2023 at 23:36
  • 1
    $\begingroup$ Why would I not be allowed to disclose the answer? I provided a very strong indication that you cannot do what you want, as it would imply P=NP. If you prefer, it is a conditional proof: $P \neq NP$ implies that there is no such 2-SAT formula. Perhaps somebody can provide a proof that does not rely on $P \neq NP$. $\endgroup$
    – Steven
    Commented Sep 7, 2023 at 0:13
  • 1
    $\begingroup$ @BernardoSubercaseaux. I did not say that NAND being universal implies that an arbitrary CNF formula can expressed an equisatisfiable NAND formula (in polynomial size/time). What I said is that if it was possible to encode $q = \overline{a \wedge b}$ in a 2-SAT subformula, then you could encode any formula $\phi$ into a 2-SAT formula (in poly time), using the fact that NAND is universal. Here is how you do that: Write $\phi$ as a polynomial size circuit in the straighforward way, replace each gate with a constant number of NAND gates, write a 2-SAT formula equivalent to that circuit. $\endgroup$
    – Steven
    Commented Sep 7, 2023 at 9:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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