NOT satisfiable 3SAT instance certificate

Question

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

Answer 1

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.