complexity theory – NOT satisfiable 3SAT instance certificate

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,cright}$, $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)))$.