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

【问题标题】：Compilers that translate verification algorithms into SAT problems将验证算法转换为 SAT 问题的编译器
【发布时间】：2011-12-12 08:02:19
【问题描述】：

SAT 是 NP-complete 的证明是一个建设性的证明，所以应该可以将它作为一个程序来实现。有人做过吗？

我正在寻找一个程序（编译器），它将程序（返回真或假）作为输入并输出 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 公式会有其他辅助变量，因此编译器必须指出哪些变量对应于证书。

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

【问题讨论】：

标签： compiler-construction np-complete satisfiability

【解决方案1】：

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

【讨论】：