2

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:

  1. 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)
  2. Repeat step 1 until you run out of places to write 0s or run out of formulas
  3. If there are 0s everywhere, the whole formula can't be satisfied
  4. 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)

Attachment

Andrej
  • 51
  • Why not ? But the problem is that you cannot handle many "variables" : above, say 6 variables ($\rightarrow 2^6$ cells), it becomes untractable... – Jean Marie Apr 30 '20 at 10:49
  • 1
    So the overall process and result is mathematically acceptable if I was lets say, doing it as a part of a proof? The main pointis, this is a speedup for smaller problems if I need to do many of them, but I'm having trouble finding anything about it, even college professors didn't give me an exact answer and directed me to ask publicly, maybe someone will know. – Andrej Apr 30 '20 at 12:02

0 Answers0