Re: Satisfiability problem compiler

Matt,
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?
Best,
Kerry


"Matt Timmermans" <mt0000@xxxxxxxxxxxxxxxxxxxxxxxxxx> wrote in message
news:wV_8e.4380$Jg5.402923@xxxxxxxxxxxxxxxxxxxxxxxx
> "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

  • Re: Satisfiability problem compiler
    ... > compiler which would (in polynomial time, ... > satisfiability problems; then the satisfiabilty-solving algorithm would ... Does anyone know of research into such a compiler? ...
    (comp.theory)
  • Need help figuring out: "CVT1100 Duplicate Resource: type ICON"
    ... I tried changing the value of typelib resource ID - I tried a whole ... Since the MSDN groups couldn't offer any enlightenment other than to say ... I commented out ALL references I got "CVT1100 duplicate resource type Dialog ... This program compiles using the 4.2 compiler - there is still a version ...
    (microsoft.public.dotnet.languages.vc)
  • Re: VACPP Compiler v3.6.5
    ... The IBM CD-ROM has four bugs. ... So there were two enviroment variables pointing to the same folder at the same time which led to the warning and error messages. ... I personally installed the VisualAge 3.00 package, and then later installed the 3.65 C compiler into the same directories. ... I personally have references to the IBM CPP directories in the ...
    (comp.os.os2.programmer.misc)
  • RE: Huge project - long build time
    ... We too are having terrible speed problems with VS.NET. ... Until the middle of last week, build times were reasonable and the compiler ... now takes 20 minutes to rebuild the system. ... > references with dll references. ...
    (microsoft.public.dotnet.general)
  • Re: behavior-preserving optimization in C, was compiler bugs
    ... any forward references to the name in the same file, ... How does a compiler know about other files? ... definitions of the same symbol in multiple object files. ... expected behaviour of the linker. ...
    (comp.compilers)