Re: Satisfiability problem compiler

In article <LGg9e.20119$hu5.1968@xxxxxxxxxxxxxxxxxxxx>,
Kerry Soileau <ksoileau@xxxxxxxxx> wrote:
>Thanks for your reply. I'm looking for references to compilers which could
>take a mathematical statement such as X + Y = Z and produce an equivalent
>SAT formula. Do you know of any such references in the literature?

The first thing to be aware of is that SAT is a decidable problem, whereas
assessing the validity of an arbitrary mathematical statement is an
undecidable problem. Therefore your project cannot possibly succeed as
stated.

The next thing to note is that even among decidable problems, there are
complexity classes that are provably beyond NP. Therefore an efficient
algorithm for SAT would not be able to solve those harder problems
efficiently.

In spite of this, there is a sense in which your project can be carried
out. Given (just about) any mathematical statement, one can convert
it into, say, the first-order language of set theory, and then ask if
there is a proof of length n of the statement from (say) the axioms
of ZFC, where n is given in unary and "length" is suitably defined.
This problem can be reduced to SAT.

The first part of this process I've just outlined, namely the
formalization of mathematical statements, is a subject of active interest
(keywords include the QED project, Mizar, automated deduction systems,
proof checkers). Doing the actual conversion to SAT is in principle
straightforward but tedious in practice, and I doubt that anyone's done
it, because the lack of an efficient algorithm for SAT, there doesn't
seem to be much practical point in implementing such a thing.
--
Tim Chow tchow-at-alum-dot-mit-dot-edu
The range of our projectiles---even ... the artillery---however great, will
never exceed four of those miles of which as many thousand separate us from
the center of the earth. ---Galileo, Dialogues Concerning Two New Sciences
.