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?