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

Question

证明SAT是np完全的是一个建设性的证明，所以它应该可以作为一个程序来实现。有人这样做过吗?

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

因此，例如，编译器可以将以下程序(以python语法显示，但我认为任何语言都可以)作为输入，并输出一个SAT公式。将SAT公式输入到SAT求解器将得到参数"certificate"的解。在这种情况下，解将是[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(没有循环)的图灵完备语言编写，但您可以使用整数和实值变量、布尔逻辑、函数、基本算术和数组。