将验证算法转化为 SAT 问题的编译器
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 公式还会有其他辅助变量，因此编译器必须指示哪些变量对应于证书。
这样的编译器已经存在吗？其中有开源的吗？
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?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您应该研究 SMT 求解器，因为它们是最接近您想要的东西。您不是使用带有 SMT（无循环）的图灵完备语言进行编写，但您可以使用整数和实值变量、布尔逻辑、函数、基本算术和数组。
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.