将验证算法转换为SAT问题的编译器

Question

SAT是NP完全的证明是一个建设性的证明,因此应该可以将它作为一个程序来实现.有没有人这样做过？

我正在寻找一个程序(编译器),它将一个程序(返回true或false)作为输入,并输出一个SAT公式.

因此,例如,编译器可以采用以下程序(以pythonic语法显示,但任何语言都适合我)作为输入,并输出SAT公式.将SAT公式提供给SAT求解器将给出参数"证书"的解决方案.在这种情况下,解决方案将是[False,True,True,True,False],表明{-3,-2,5}是一个解决方案.

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

显然,输出SAT公式将具有其他辅助变量,因此编译器必须指示哪些变量对应于证书.

这样的编译器已经存在吗？他们中的任何一个都是开源的？

Answer 1

您应该研究 SMT 求解器，因为它们是最接近您想要的东西。您不是使用带有 SMT（无循环）的图灵完备语言进行编写，但您可以使用整数和实值变量、布尔逻辑、函数、基本算术和数组。