0
$\begingroup$

What is the goal of the SAT Problem?

  • Check if it is possible to have output '1'?

  • Above + find the right combination of inputs for that?

Witch one?

Cheers

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ There is a nice article on Wikipedia: en.wikipedia.org/wiki/Boolean_satisfiability_problem. $\endgroup$
    – Yuval Filmus
    Commented Mar 7, 2018 at 13:07
  • 1
    $\begingroup$ I don't want to discourage you asking questions, but you have to do some research on your own before asking questions. You did not point out why you did not understand the goal of SAT problem. If you do, people know that you worked on it before asking it. $\endgroup$
    – alim
    Commented Mar 9, 2018 at 6:42

2 Answers 2

Reset to default
2
$\begingroup$

In computational complexity, we usually think of SAT as a decision problem: given a CNF, decide whether there is a truth assignment that satisfies it. There is also a search version of SAT: given a CNF, either find a satisfying assignment, or state that the formula is unsatisfiable. SAT solvers consider a third version: given a CNF, either find a satisfying assignment, or a proof that the formula is unsatisfiable.

There are several relations between the various versions. First, if you solve the decision version, you can also solve the search version. The idea is to find the lexicographically smallest satisfying assignment. Assuming that the variables are $x_1,\ldots,x_n$, we first substitute $x_1=0$ and check whether the resulting formula is still satisfiable. If so, we continue on to $x_2$. Otherwise, we substitute $x_1 = 1$ (the formula must remain satisfiable) and continue on to $x_2$. After $n-1$ more such steps we uncover a satisfying assignment.

Another relation is that if you can solve the search version that you can also solve the SAT solver version. The idea is that if the algorithm for the search version states that the CNF is unsatisfiable, then the transcript of the algorithm serves as proof that the CNF is indeed unsatisfiable. So these two versions are essentially equivalent.

Improve this answer
$\endgroup$
0
$\begingroup$

Depends if you need to know the value attributions or not.

Deciding the output is always the goal of SAT problem. Deciding the values that lead to the output is something extra.

Notice that if you can decide if the output is 1 then you can decide the input that generates the solution.

Improve this answer
$\endgroup$

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