A script that checks if a given formula is satisfiable
This script was created in order to solve the satisfiability problem. It outputs the formula in disjunctive normal form
and informs you whether it's satisfiable. The formula is not satisfiable if all of its elementary components contain a pair of opposite literals.
To achieve it, the script applies suitable laws and definitions:
- Def. of implication
- Def. of equivalence
- DeMorgan's laws
- Double negation law
- Distributive law
Signs below represent logical conjunctions:
|- disjunction (or)&- conjunction (and)<>- If and only if>>- implication~- negation
Here I'm gonna show how the script applies the laws and definitions on a simple example.
Formula: (p<>q)>>p&q
- Def. of equivalence
(p>>q)&(q>>p)>>p&q - Def. of implication
(~p|q)&(q>>p)>>p&q - Def. of implication
(~p|q)&(~q|p)>>p&q - Def. of implication
~[(~p|q)&(~q|p)]|(p&q) - DeMorgan's laws
~(~p|q)|~(~q|p)|(p&q) - DeMorgan's laws
(p&~q)|~(~q|p)|(p&q) - DeMorgan's laws
(p&~q)|(q&~p)|(p&q)
Formula is now in disjunctive normal form and the script proceeds to check if it's satisfiable.
The verdict is that it is indeed satisfiable.
It's very simple to use it as it doesn't require any 3rd party libraries. Script was written in Python 3.8.1. There's no formula validation so make sure you input a correct formula.
There are tests, written using unittest, which are to ensure that no code improvements would generate wrong answers. There's 9 formulas which brings us to 54 unit tests.