0
$\begingroup$

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.

Also similar question asked at this link.

$\endgroup$
5
  • 3
    $\begingroup$ 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? $\endgroup$
    – Steven
    Nov 28 '21 at 10:57
  • $\begingroup$ 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/… $\endgroup$
    – Ahmad
    Nov 28 '21 at 11:10
  • $\begingroup$ My question come from that link. $\endgroup$
    – Ahmad
    Nov 28 '21 at 11:10
  • 1
    $\begingroup$ The question is not asking to just decide whether $\phi$ is satisfiable. It is asking to compute a satisfying assignment. $\endgroup$
    – Steven
    Nov 28 '21 at 11:13
  • $\begingroup$ Thank you, so how it's possible to do it? $\endgroup$
    – Ahmad
    Nov 28 '21 at 11:18
1
$\begingroup$

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$.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.$$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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