How to create an algorithm for determining Boolean Tautologies

Question

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

Answer 1

The problem to detect a tautology is equivalent to the boolean satisfiability problem which is sadly np-complete for general instances. You can easily convert tautology detection into SAT problem by negating the boolean equation and check its satisfiability , if the negated equation is unsatisfiable then the original equation must be a tautology.

What you can do :-

1. Use lex & yacc parser tools to generate a grammer to parse a equation.
2. Evaluate the negation of the equation using de-morgan's law.
3. Give the negated eqaution to a standard SAT solvers.

Note: If your equation is reducible to 2-SAT then there is linear time algorithm .