So i am right now exploring some topics in a proof course and it occurred to me to try to create a boolean tautology solver. I would like an algorithm that is more efficient than brute force.
Problem Statement:
given a string of '(', ')', '[and]', '[or]', ! and pieces of text that denote variable names (which by definition cannot include parenthetical marks brace marks or ! marks) which must be surrounded by a pair of parenthesis
The words 'TRUE' and 'FALSE' are also reserved
determine if the boolean string is well-formed and if so, is it a tautology
ex: (alpha)[and](beta)
is well formed and not a tautology because if: alpha = false and beta = true is a counter example
ex: (alpha)[or]!(alpha)
is well formed and a tautology because ((X)[or]!(X))
is by definition a tautology
ex: ((alpha)[or]((beta)[or]!(beta)))
is well formed since (beta)[or]!(beta)
is true and ((alpha)[or](TRUE))
is always true
ex: ((alpha[and](beta))
is not well formed
Some ideas I had for this was to begin by forming a parenthetical tree. Since every statement will be encapsulated by parenthesis before it can be applied to a [or], [and], or [!] operator what I can do is partition the string into its separate highest level blocks enclosed by parenthesis (clause1)(clause2) to generate 2 nodes of a tree pointing to the high level node
Each node contains information about whether it has a ! attached to it's front, and if it has nodes below, what operator is used to unify those two nodes
This tree could be quickly generated to reduce the statement to individual literals and easily verify if the statement is well-formed (are there an equal number of ( as ) and does every [or] and [and] have two statements surrounding and a pair of encapsulating parenthesis around these two statements.
Now my plan was to systematically crawl up to nodes that do have a (!) value and distribute the not via DeMorgan's laws. If I am ever forced to do something along the lines (x and !x) I have immediately found a contradiction and can abort.
I'm still not perfectly clear what must happen at this stage however
O(2^n)
performance hit though :/