# How it's possible decide CNF by having a turing machine that decide SAT?

Suppose we have a Turing machine $$M$$ as black box that decide $$SAT$$ problem. Now suppse we have a $$CNF$$ formula $$\phi$$ with $$n$$ variables. How it possible checking satisfiblity of $$\phi$$ and then finding that assignment with at most $$2n+1$$ times using $$M$$?

I know that every $$SAT$$ instance can comverted to $$CNF$$ clauses so i think we can do it recursively to checking satisfiblity and then finding it, but i get stuck to formulate it that how we can do it.

• The SAT problem is defined as the problem of deciding whether a boolean formula (usually in conjunctive normal form) is satisfiable. So why can't you just invoke $M$ once on your input CNF formula? Commented Nov 28, 2021 at 10:57
• It's also ambiguous for me, look at exercise 3.1 section a from the following link archive.model.in.tum.de/um/courses/complexity/SS10/exercises/… Commented Nov 28, 2021 at 11:10
• My question come from that link. Commented Nov 28, 2021 at 11:10
• The question is not asking to just decide whether $\phi$ is satisfiable. It is asking to compute a satisfying assignment. Commented Nov 28, 2021 at 11:13
• Thank you, so how it's possible to do it? Commented Nov 28, 2021 at 11:18

First of all, check whether $$\phi$$ is satisfiable using $$M$$. If it is, you can find a satysying assignment as follows:

For each variable $$x$$ of $$\phi$$ do the following:

• Set $$x$$ to true. Simplify $$\phi$$ to remove $$x$$ (if a clause contains $$x$$ then you can delete the clause, if a clause contains $$\overline{x}$$ then you can delete $$\overline{x}$$ from the clause) and let $$\phi_x$$ be the resulting formula.
• Check whether $$\phi_x$$ is satisfiable using $$M$$.
• If $$\phi_x$$ is satisfiable, set $$\phi=\phi_x$$ and continue with the next variable.
• Otherwise $$x$$ must be false. Set $$x$$ to false and update by $$\phi$$ by removing all occurrences of $$x$$ or $$\overline{x}$$ (if a clause contains $$\overline{x}$$ then you can delete the clause, if a clause contains $$x$$ then you can delete $$x$$ from the clause). Then continue with the next variable.

At the end of this process, the values assigned to the variables are a satisfying assignment of the input formula. This requires at most $$n+1$$ invocations of $$M$$.

If you want to decide whether a CNF formula is satisfiable or not you can simply decide it with one invoke of $$M$$ on your formula. But if you want to calculate its satisfying assignment, your problem is a search problem not a decision problem. To do that you can simply invoke $$M$$ on $$\phi [True/x_i]$$ (substituting variable $$x_i$$ with value $$True$$) for each variable $$x_i$$ recursively until no more variables left. It is easy to see that if the result is $$Accept$$, you can assign $$True$$ to $$x_i$$ and $$False$$ otherwise and recurse on the new formula $$\psi= \phi [v(x_i)/x_i]$$. If you want more details about how to formulate it you can check Arrora complexity book for this purpose.

You can actually do it in at most $$n+1$$ queries. Just first check that the whole sentence is satisfiable, then play guess-and-check for each variable. Writing $$|\phi|$$ for the number of variables in the sentence $$\phi$$,

\mathit{cnf\_and\_sat}(\phi)=\left\{\begin{align*} &\mathit{cnf}(\phi,|\phi|)&\mathit{sat}(\phi)\\ &\mathbf{unsat}&\mathrm{otherwise} \end{align*}\right.

\mathit{cnf}(\phi,n)=\left\{\begin{align*} &\emptyset&n=0\\ &\{x_n\}\cup\mathit{cnf}(\phi\land x_n,n-1)&n\ne0\enspace\mathrm{and}\enspace\mathit{sat}(\phi\land x_n)\\ &\{\overline{x_n}\}\cup\mathit{cnf}(\phi\land\overline{x_n},n-1)&\mathrm{otherwise} \end{align*}\right.