0
$\begingroup$

A logical formula is unsatisfiable if and only if for the formula to be true, at least one of its variables must be both true and false.

I discovered SAT today, and wanted to try my hands at solving it. I arrived at the above statement as a general principle for any attempt I want to make at solving SAT. Is the principle true?

Improve this question
$\endgroup$
7
  • 1
    $\begingroup$ Unclear what it states. A logical formula is unsatisfiable if there is no assignment of its variables that turns the fotmula to the logical true. I hope you are aware it is NP complete. $\endgroup$ – fade2black Jul 26 '17 at 13:24
  • $\begingroup$ @fade2black, I've clarified the question. $\endgroup$ – Tobi Alafin Jul 26 '17 at 13:34
  • $\begingroup$ Have you tried proving the statement? $\endgroup$ – adrianN Jul 26 '17 at 13:38
  • $\begingroup$ That condition is not enough. A CNF formula is satisfiable if all of its clauses is true. It is possible that all its variables take false value while the formula may be true. $\endgroup$ – fade2black Jul 26 '17 at 13:39
  • $\begingroup$ I don't really have any training in formal proofs. So I may have an argument, but I'm not sure if it meets the standards of mathematical rigour others may adopt. $\endgroup$ – Tobi Alafin Jul 26 '17 at 13:39
5
$\begingroup$

Your statement is not very precise, because you don't define "requires" but it looks like you're close to discovering resolution proofs. Using the resolution rule you can derive new clauses from your formula. If you can derive both x and not x, then the formula is not satisfiable.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks for the link, will check it out. I've edited the question as well. $\endgroup$ – Tobi Alafin Jul 26 '17 at 13:58

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.