Re: Satisfiability problem compiler

"Kerry Soileau" <ksoileau@xxxxxxxxx> wrote in message
news:lLE8e.12123$hu5.9717@xxxxxxxxxxxxxxxxxxxxxxx
> If tomorrow somebody invented an algorithm to solve any satisfiability
> problem in polynomial time, a logical next step would be to develop a
> compiler which would (in polynomial time, or in some efficient way)
> convert mathematical questions into their corresponding formulations as
> satisfiability problems; then the satisfiabilty-solving algorithm would
> produce the solution. Does anyone know of research into such a compiler?
> Thanks.
> Kerry Soileau

The design of such a compiler is essentially the method by which Stephen
Cook originally proved that SAT was NP-complete. From an NDTM, an input,
and a polynomial bound on its running time, his procedure would produce a
SAT instance of a size proportional to the square of that bound.

The paper is here:
http://portal.acm.org/citation.cfm?id=805047&coll=ACM&dl=ACM&CFID=42307909&CFTOKEN=31853645

It's actually not too difficult to do the same sort of thing with a
friendlier programming language. Given a polynomial-time solution-checking
program, you replace every bit of the solution and program state with a
variable. Run the program until the end of its time bound by introducing
new variables for any bit that might change during a time step, and
introducing CNF clauses to ensure the proper evolution from one time step to
the next. Finally, add the clause asserting that the program returns
success before the bound expires, and you have a CNF formula that is
satisfiable iff there is a solution that would cause the program to return
success.

The SAT instances you get out of such a thing, as with Cook's original
procedure, end up being about as big as the square of the time bound on the
program you're converting.

--
Matt


.

Relevant Pages

  • Satisfiability problem compiler
    ... If tomorrow somebody invented an algorithm to solve any satisfiability ... compiler which would (in polynomial time, or in some efficient way) convert ... Does anyone know of research into such a compiler? ...
    (comp.theory)
  • Re: Satisfiability problem compiler
    ... take a mathematical statement such as X + Y = Z and produce an equivalent ... Do you know of any such references in the literature? ... >> compiler which would (in polynomial time, ... Does anyone know of research into such a compiler? ...
    (comp.theory)