Given a NOT satisfiable 3SAT instance, that we say $S$. Suppose that $M$ is a minimal subset of clauses of $S$ such that $M$ is NOT satisfiable. Say $X$ the subset of variables of $S$ that belong to the clause of $M$. For each Boolean values combination of the variables of $X$, we have a clause of $M$ that is false, because $M$ is NOT satisfiable.

The question is: is $M$ a polynomial certificate that $S$ is NOT satisfiable? I mean: if we have $M$, we can check that, for each possible Boolean value of the variables that are in $X$, there is a false clause in $M$. This means that $M$ is a certificate that $S$ is NOT satisfiable. Because each clause is false for only one Boolean value of the variables that are in the clause and becasue $M$ is minimal, the number of cases, that we have to check to verify that $M$ is NOT satisfiable, is the cardinality of $M$ (i.e. the number of clauses in $M$). Threfore the complexity of the certificate is linear on the number of clauses of $M$ (therefore linear on the number of clauses of $S$).

Here an example.
If $X=\left\{a,b,c\right\}$, $M$ contains all possibile combinations, three by three, of $\left\{a,b,c,\bar{a},\bar{b},\bar{c}\right\}$ ($9$ literals in all), without that a variable and its negation appear in the same clause (it would be a tautology). Therefore the number of clauses of $M$ is exponential on the number of the variables of $X$, but the number of clauses of $M$ is at most the number of clauses of $S$. In other word we have $cardinality(X)=O(\log(numberClauses(S)))$.


A CNF which is not satisfiable is usually called unsatisfiable. A CNF which is unsatisfiable but becomes satisfiable if we drop any clause is minimally unsatisfiable.

Papadimitrious and Wolfe constructed, in their paper The complexity of facets resolved (Lemma 1), a polynomial time reduction $f$ from CNFs to CNFs such that:

  • If $\varphi$ is satisfiable then $f(\varphi)$ is satisfiable.
  • If $\varphi$ is unsatisfiable then $f(\varphi)$ is minimally unsatisfiable.

It is likely that this can be extended to a reduction from 3CNFs to 3CNFs.

This reduction shows that the minimally unsatisfiable case is the "hardest". In particular, if there is an efficient way to check that a minimally unsatisfiable CNF is unsatisfiable, then P=NP.

  • $\begingroup$ Ok, but what about my question? In particular, is the number of the variables in a minimally unsatisfiable 3CNF $O\log(numberClauses)$? $\endgroup$ – Mario Giambarioli Apr 5 at 14:59
  • 1
    $\begingroup$ No. Take, for example, $x_1 \land (\lnot x_1 \lor x_2) \land (\lnot x_2 \lor x_3) \land \cdots \land (\lnot x_{n-1} \lor x_n) \land \lnot x_n$. $\endgroup$ – Yuval Filmus Apr 5 at 15:02
  • $\begingroup$ A more exciting example is Tsietin contradictions on 3-regular graphs, which are also minimally unsatisfiable. $\endgroup$ – Yuval Filmus Apr 5 at 15:04

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.