Are Karnaugh maps "good enough" or mathematically acceptable to prove a CNF formula can't be satisfied instead of using propositional logic resolution? This method also shows all possibilities to satisfy the formula if there are any.
Picture attached shows a solution for the following formula: (a ∨ ¬b) ∧ (b ∨ ¬c) ∧ (a ∨ c) ∧ (¬a ∨ d) ∧ (¬a ∨ b ∨ ¬d); converting between {∨, ¬, ∧} to {+, ̅ ,.} is trivial and just a personal preference (using the latter looks more readable to me coming from IT)
The process of solving is as follows:
- Select each individual formula from the CNF form and write 0s to the corresponding row/column (negating the original literals gives exactly the place where they should be, that's just a helper process as seen in the picture attached)
- Repeat step 1 until you run out of places to write 0s or run out of formulas
- If there are 0s everywhere, the whole formula can't be satisfied
- If there are empty places, those are values for which the formula can be satisfied and we can write them down (1111 and 1101 for the case in the picture)
