4

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

Improve this question
1
  • Well the most trivial method would be to instantiate each variable as true or false and reduce the (now constant) AST. This has a brutal O(2^n) performance hit though :/
    – daniel gratzer
    Jul 22, 2014 at 5:35

1 Answer 1

Reset to default
7

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 .

Improve this answer
4
  • 1
    Lex and yacc would be a mistake for something so simple, but it does need a simple parser and tree-builder.
    – david.pfx
    Jul 22, 2014 at 11:08
  • @david.pfx i think you are right.
    – Vikram Bhat
    Jul 22, 2014 at 11:19
  • That also means something like this: ics.uci.edu/~eppstein/280e/001121.pdf could be used to try to make the time complexity nicer?
    – Sidharth Ghoshal
    Jul 22, 2014 at 13:33
  • @frogeyedpeas yes sure you can use any such algorithm but preferably an already present library in your favorite programming language , Your important goal now is to build a parser and negate the equation which is possible in polynomial time.
    – Vikram Bhat
    Jul 22, 2014 at 14:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.