0
$\begingroup$

In this question

Farewell Stack Exchange suggested to use karnaugh maps to solve the satisfiability problem by simplifying the entire/whole boolean formula by simplifying subformulas until you have reached a contradiction or the current boolean formula cannot be simplified anymore.

ratchet freak answered that this method doesn't work on all inputs.

I have new idea:

Instead of using karnaugh maps let's use Quine McCluskey algorithm to simplify the entire/whole boolean formula by simplifying subformulas and if you have reached a contradiction then return "unsatisfiable" as answer.

If the current boolean formula cannot be simplified anymore then return "satisfiable" as answer.

Does the new algorithm work?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

If you're planning to apply this to each subformula with 16 variables:

No, that doesn't work for the same reason given in ratchet freak's answer. As the Wikipedia article states, Quine McCluskey is functionally identical to Karnaugh maps, so your idea has the exact same problem.

If you're planning to apply this to the entire formula:

No, that doesn't work. Quine McCluskey outputs a DNF formula or CNF formula. That alone doesn't tell you whether the resulting formula is satisfiable or not. You haven't said how to test whether there is a "contradiction"; testing for a "contradiction" is exactly the problem of testing satisfiability, so this hasn't gained you anything.

In any case, Quine McCluskey takes exponential time in the worst case. Therefore, this approach is inefficient for formulas of any substantial size. As far as asymptotic worst-case running time is concerned, you might as well just enumerate all possible assignments and see if any of them satisfy the algorithm -- that also takes exponential time.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Did you read at all Farewell Stack Exchange's question that I linked to in my question before answering at all? Farewell Stack Exchange's idea was to simplify subformulas with at most 16 boolean variables until gradually the whole formula has been simplified. He suggested to use karnaugh maps to do the simplifications. I suggest to use Quine McCluskey algorithm instead of karnaugh maps to simplify subformulas until the whole formula has been simplified gradually. You have reached a contradiction if the simplified subformula is False or 0. $\endgroup$
    – user82913
    Jan 24, 2018 at 1:33
  • $\begingroup$ My idea is to use Quine McCluskey algorithm on subformulas with much lesser boolean variables and clauses, inspired by Farewell Stack Exchange, instead on all input boolean formula, so that the simplification of the entire input boolean formula will be gradual and done in polynomial time. Quine McCluskey algorithm is called more than once. I am asking if this can work or not. $\endgroup$
    – user82913
    Jan 24, 2018 at 1:40
  • 2
    $\begingroup$ @user82913, that doesn't work for the same reason that it doesn't work with Karnaugh maps. I suggest you spend some more time understanding ratchet freak's answer and understanding Quine McCluskey. As the Wikipedia article states, Quine McCluskey is functionally identical to Karnaugh maps. $\endgroup$
    – D.W. ♦
    Jan 24, 2018 at 2:19

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.