Satisfiability problem compiler

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


.

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)
  • Re: sat to horn sat
    ... But maybe you want an algorithm that converts a sat instance you ... I'd just like to see an example of reduction from sat to horn sat. ... Tricky part is to define R so that it applies to all to sat instances preserving satisfiability. ... And surely there exists one that satisfies the requirement "X is satisfiable iff Ris satisfiable". ...
    (sci.math)
  • Re: sat to horn sat
    ... |>apoph wrote: ... |>>Is there an algorithm that turns sat instances into horn sat? ... R is not trivial in a sense that it first decides X and then outputs some fixed satisfiable or unsatisfiable horn sat instance accordingly to the satisfiability of X. ...
    (sci.math)
  • Re: why not just publish truth table?
    ... The problem "satisfiability" is NP complete. ... then every algorithm takes too long. ... too much time to be practical [which is certainly untrue, ... with the context of the previous sentence. ...
    (sci.math)
  • Re: why not just publish truth table?
    ... The problem "satisfiability" is NP complete. ... then every algorithm takes too long. ... REAL-TIME solvers) designed for particular tasks and performing well. ... with the context of the previous sentence. ...
    (sci.math)