0
$\begingroup$

I'm self studying complexity theory and want to prove that SAT is in NP, so I came up with this verifier for SAT:

\begin{align*} V &= \text{"On input $w = \langle \phi, c \rangle$}:\\ & \quad \text{1. Test whether $c$ is an assignment for $\phi$} \\ & \quad \text{2. Test whether $c$ satisfies $\phi$}\\ & \quad \text{3. If both pass, accept; otherwise, reject."} \end{align*}

It seems that this is supposed to be an easy question but how can I show that this runs in polynomial time in the size of the input, i.e., $|\langle \phi, c\rangle|$?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

You just need to show that you can evaluate $\phi$ in polynomial-time. This is clearly true for any reasonable encoding of $\phi$ and $c$, but the details depend on the specific encoding you choose.

One of the many possible "natural" encodings could be as follows: $\phi$ is encoded by specifying the number of variables $n$, the number of clauses $m$, and list of clauses, where each clause is a list of literals. Each literal is just a pair whose first element is the index (between $1$ and $n$) of a variable and the second elements is a boolean that encodes whether the variable is negated. The assignment $c$ is an array of $n$ boolean values, the $i$-th value is the truth value of the $i$-th variable.

Assume that you already checked that the input is a valid encoding.

Then you can just scan the list of clauses. For each clause, scan the list of literals. For each literal check whether the literal is positive and the corresponding variable is set to true in $c$, or the literal is negated and the variable is set to false. If no literal in the clause satisfies the above conditions, reject. If you run of clauses without rejecting, accept.

This takes time proportional to $m+n$ on the RAM model. If you want to use a Turing machine, describing the algorithm is more annoying and depends on even more fine-grained details of the encoding, but it can be done.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ I think you are considering CNF-SAT, and not the general SAT problem (though the idea is similar). $\endgroup$
    – Nathaniel
    Nov 7, 2022 at 17:58
  • 1
    $\begingroup$ @Nathaniel, you are right. Then please interpret the answer as an intuitive argument to convince the reader that "it can be done". A convenient encoding of $\phi$ for general SAT formulae could be in the form of a binary expression tree. The algorithm works in phase. At each phase one not-yet-evaluated vertex having only evaluated vertices as children is located and it replaced with its corresponding truth value. At the beginning only leaves are "evaluated". At the end, the value of $\phi$ is the value of the root. The time is quadratic in the tree size (one can do better but this suffices). $\endgroup$
    – Steven
    Nov 7, 2022 at 18:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.