# algorithm for checking satisfiability

In order to prove that SAT is in NP, I need to come up with a polynomial time verfier (an algorithm). The Cooks Levin Theorem uses a non-deterministic Turing machine but that's not what I am looking for.

The idea of the algorithm could be that we put in the values and calculate the answer. Then, we check whether the answer is 1 or not. However, I am unable to understand how I could write a psuedocode for the 'putting in values' part and then show that it's polynomial for sure.

if x = 1:
accept
else:
reject


This could be in O(1). But what about the remaining part?

• usually we consider the input to a sat problem to be written in DNF (en.wikipedia.org/wiki/Disjunctive_normal_form) meaning you get a list of closures $C_i$ where each closure is again a list of (possibly negated) literals. The solution is given as a mapping that maps every literal $x_j$ to a boolean value (0 or 1). Aug 28 '20 at 10:29
• Now to compute the value of the whole formula you first compute the value of every value (which is just the OR of every literal $x_j$ value contained in it ) and in the end AND all closure values. Aug 28 '20 at 10:31
• SAT is normally defined to accept its input as a CNF formula, not DNF.
– D.W.
Aug 30 '20 at 5:03

Here is how I would do it:

Algo: Verifier for DNF-SAT problem given as array of closures and a possible mapping of literals to booleans
Input:
Array of closures: [$$C_1$$,$$C_2$$,...,$$C_m$$]
where $$C_j \subseteq \{x_1,...,x_n,\neg x_1, ... \neg x_n\}$$
(Certificate) Array $$M$$ where $$M_i$$ is the boolean value of literal $$x_i$$
Output: true or false

for $$i = 1$$ to $$m$$:
value = true
for literal in $$C_i$$:
if literal == $$x_i$$:
value = value or $$M[i]$$:
else if literal == $$\neg x_i$$:
value = value or (not $$M[i]$$)
if not value:
return false
return true


Note: the math notation is indented and commonly used in pseudocode sadly cs stackexchange doesn't support it

• ok the output 1 or true can only come out if the AND of all the values of the individual clojures is true. AND operations are only true/1 if all arguments are true/1 meaning that as soon as the value of one clojure is false/0 we know that the AND of all clojures is false and we can already return false. If no clojures are false (the loop doesn't break) all of them must be true and we can return true. Aug 28 '20 at 12:51