# how to polynomially check if a given boolean formula is unsatisfiable

Since SAT is np-complete, there is a polynomial algorithm to check if a given solution for any particular formula is correct. Just substitute the values and solve. But what if one claims that the given formula is unsatisfiable, is there a polynomial way to check if the claim is true... Am i missing something ?

NP only requires you to have a polynomial size proof for "yes" instances.

co-NP is the class of problems that requires polynomial size proofs for "no" instances.

SAT is in NP, but is not known to be in co-NP. Whether NP = co-NP is an open problem (and proving that SAT is in co-NP would resolve this problem in the affirmative).

So to answer the question in your title, how to polynomially check if a given boolean formula is unsatisfiable: no one knows whether that could be done in general.

• " no one knows whether that could be done in general. " you mean in polynomial time right ? Commented Mar 5 at 12:47
• Also, " NP only requires you to have a polynomial size proof for "yes" instances. " , i think that's exactly what i was looking for, can you give some link to any website or maybe any book where it mentions, I want some sort of formal proof, cuz i looked the definition for np problems, and no website i checked states in this form - NP only requires you to have a polynomial size proof for "yes" instances....... so i desperately want some sort of authentic source where it mentions it in this way, if you don't mind Commented Mar 5 at 12:50
• @AlexMatyasaur Yes, in polynomial time + size for the certificate. Regarding an authoritative source, any book on complexity should have this in the definition of NP. You could also read the formal definition on Wikipedia precisely: note how the requirements are different for the "yes" instances ("For all x in L") and for the "no" instances ("For all x not in L"). For the "no" instances it only requires that it doesn't give false positive proofs, not that it proves the instance is in fact a "no" instance.
– orlp
Commented Mar 5 at 12:57
• Also, "I want some sort of formal proof" - this is not possible. This is part of the definition of NP, not some proven property.
– orlp
Commented Mar 5 at 12:59
• by formal proof i meant some source obviously; thanks for the wikipedia subsection link... i was confused if definition of np includes polynomial certificates for no-instances as well..... Commented Mar 5 at 13:08

We don't know for sure, but most people expect the answer is "no". In particular, assuming NP != co-NP (as is a commonly held conjecture), the answer is "no".

Checking that a formula is satisfiable (and exhibiting a proof that it is) is a NP-complete problem. Checking that a formula is unsatisfiable (and exhibiting a proof that it is not satisfiable) is a co-NP-complete problem.

• unsatisfiability , imo, is fundamentally different than SAT. A formula is satisfiable by only a finite number of solutions, a single instance is enough to prove the formula is satisfiable, on the other hand, if a formula is unsatisfiable, we can never know just be checking for each solution cuz they will be infinite, i don't think we can ever know if a formula is unsatisfiable polynomially....... Commented Mar 10 at 12:30