A sound, fast and hence incomplete boolean expression simplifier in pure python.
Basic usage with examples:
>> from simbool.proposition import Prop
>> from simbool.simplify import simplify
# Creating 3 atomic propositions
>> A, B, C = [Prop(x) for x in "ABC"]
# Simplifing some expressions
>> simplify(~A | (C & (~(B & ~C) | A)))
~A | C
>> simplify((C & A) | (C & B) | (A & ~B))
(A & ~B) | (C & B)
# Proving simple theorems ( > is the logical implication)
>> P = (A > B) | (B > A)
>> simplify(P)
True
# Transitivity of implication
>> P = ((A > B) & (B > C)) > (A > C)
>> simplify(P)
True
>> P = ((A > B) & (B > A)) > ((A & B) | ~(A | B))
>> simplify(P)
True
This is not based on the Quine-McCluskey algorithm. Instead, it applies various formal simplification steps until reaching a fixed point. The output is guaranted to be at most as complex as the input.
The following is a uniform random-3-SAT instance from the phase transition region, with 20 variables and 91 clauses, retrieved from this SAT benchmark. With the default settings, simplify() runs for about 6 minutes on my 2GHz i7 machine.
>> P = (C | L | ~B) & (~P | I | O) & (P | C | ~K) & (I | M | ~O) & (I | ~Q | O) & (~R | ~T | K) & \
(S | ~E | ~R) & (A | J | ~S) & (~H | ~I | D) & (S | ~R | D) & (~P | R | ~D) & (~I | ~B | S) & \
(A | ~I | ~E) & (A | S | ~T) & (T | ~N | ~O) & (K | ~R | C) & (~A | ~M | ~E) & (I | Q | ~S) & \
(I | ~K | N) & (A | ~T | ~G) & (A | ~R | N) & (~B | L | ~G) & (~A | ~S | ~Q) & (~H | L | ~E) & \
(~H | ~Q | ~F) & (~Q | M | ~E) & (J | G | N) & (L | ~N | ~G) & (B | ~K | ~O) & (~Q | L | ~G) & \
(~Q | ~K | T) & (~P | ~J | K) & (~P | ~T | G) & (I | T | D) & (~B | C | ~M) & (I | ~E | T) & \
(Q | S | E) & (~I | M | O) & (~E | O | L) & (~J | B | ~R) & (Q | K | ~S) & (Q | G | ~O) & \
(C | R | ~E) & (~P | D | ~E) & (~J | R | M) & (~A | T | N) & (Q | ~I | ~L) & (J | ~M | O) & \
(~R | ~B | T) & (J | ~S | ~O) & (~S | E | ~M) & (~L | ~M | ~N) & (~P | ~A | ~O) & (H | ~J | ~K) & \
(J | ~N | ~S) & (~R | ~D | N) & (~K | L | ~G) & (~J | D | ~O) & (~P | T | ~O) & (Q | ~I | G) & \
(P | J | ~G) & (H | ~J | ~L) & (T | D | L) & (A | P | Q) & (~B | ~F | ~O) & (Q | ~B | L) & \
(R | L | ~S) & (A | K | F) & (I | ~A | ~E) & (~I | ~D | ~M) & (K | ~E | ~N) & (~L | E | ~O) & \
(S | K | N) & (I | A | F) & (K | ~C | L) & (~P | T | N) & (J | G | F) & (~C | D | ~O) & \
(~H | S | ~E) & (~Q | ~S | ~E) & (Q | E | ~F) & (J | ~M | ~G) & (Q | ~B | ~C) & (~H | ~E | ~O) & \
(~D | J | M) & (L | ~F | N) & (~H | D | G) & (R | D | O) & (~C | ~F | ~O) & (~H | ~B | ~M)
>> simplify(P)
((A & ((~I & (J | F) & M & (~H | ~F) & D) | (~H & ~J & (I | M) & ~D & F)) & ~R & ~S & ~C & ~B & ~K) | \
(C & B & D & I & H & K & J & S & R & ~A & ~F & ~M)) & ~E & O & N & Q & ~L & T & ~G & ~P