Compilers that translate verification algorithms into SAT problems

Question

The proof that SAT is NP-complete is a constructive proof, so it should be possible to implement it as a program. Has anyone done this?

I'm looking for a program (a compiler), that takes as input a program (which returns true or false) and outputs a SAT formula.

So, for example, the compiler could take the following program (show in pythonic syntax, but any language is fine with me), as input, and output a SAT formula. Feeding the SAT formula to a SAT solver would give a solution to the parameter "certificate". In this case, the solution would be [False, True, True, True, False], indicating that {-3, -2, 5} is a solution.

def verify(certificate):
  problem = [-7, -3, -2, 5, 8]
  sum = 0
  for (x, b) in zip(problem, certificate):
    if b:
      sum += x
  return sum == 0

Obviously the output SAT formula would have other auxiliary variables, so the compiler would have to indicate which variables correspond to the certificate.

Do such compilers already exist? Are any of them open source?

score 3 · Answer 1 · answered Jan 26 '12 at 19:57

You should look into SMT solvers, as they are the closest thing available to what you want. You're not writing in a Turing complete language with SMTs (no loops), but you can work with integer and real valued variables, Boolean logic, functions, basic arithmetic and arrays.

Compilers that translate verification algorithms into SAT problems

1 Answers1