如何将一系列数学约束转化为SAT或SMT问题并得到答案？
如何将一系列数学约束转化为SAT或SMT问题并得到答案？
提问于 2017-05-20 02:18:02
我有一套武断的约束。例如：
A, B, C and D are 8-bit integers.
A + B + C + D = 50
(A + B) = 25
(C + D) = 30
A < 10我可以把它转换成一个可以由picosat解决的SAT问题(我不能让minisat在我的Mac上编译)，也可以转换成一个CVC4可以解决的SMT问题。要做到这一点，我需要：
- 将这些方程映射到布尔电路中。
- 将将军澳的转换应用于电路，并将其转换为DIMACS格式。
我的问题：
- 我用什么工具进行电路转换？
- 电路的文件格式是什么，哪些是常用的？
- 我用什么工具把电路转换成DIMACS格式？
回答 3
Stack Overflow用户
回答已采纳
发布于 2018-11-18 23:32:26
在MiniZinc中，您只需编写一个约束编程模型：
set of int: I8 = 0..255;
var I8: A;
var I8: B;
var I8: C;
var I8: D;
constraint A + B + C + D == 50;
constraint (A + B) = 25;
constraint (C + D) = 30;
constraint A < 10;
solve satisfy;由于使用25 + 30 > 50，无法满足示例约束。
Z3的Python接口将允许以下内容：
from z3 import *
A, B, C, D = Ints('A B C D')
s = Solver()
s.add(A >= 0, A < 256)
s.add(B >= 0, B < 256)
s.add(C >= 0, C < 256)
s.add(A+B+C+D == 50)
s.add((A+B) == 25)
s.add((C+D) == 30)
s.add(A < 10)
print(s.check())
print(s.model())Stack Overflow用户
发布于 2017-05-20 05:29:53
概念上
建立一个电路，然后应用Tseitin变换。
您需要将加法和比较运算符表示为布尔逻辑。有一些标准的方法来建立一个电路为两个补码加法和两个补码比较.
然后，使用Tseitin变换将其转换为SAT实例。
在实践中
使用SAT前端，为您完成此转换。Z3会帮你处理的。STP也是。(这种转换有时被称为“钻头爆破”。)
Stack Overflow用户
发布于 2018-11-20 01:15:59
所以我有个答案。有一个名为基于SAT的约束求解器的程序，它将一系列约束作为S表达式，将整个过程转换为DIMACS文件，运行SAT求解器，然后将SAT求解器的结果转换回约束的结果。
糖是由田村桥幸( Naoyuki )开发的，用来解决数学难题，比如数独谜题。我发现编写复杂约束并运行它们非常简单。
例如，要找到625的平方根，可以这样做：
(int X 0 625)
(= (* X X) 625)第一行表示X从0到625。第二行说X*X是625。
这可能不像Z3那么简单和优雅，但它确实工作得很好。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/44101068
复制相关文章
相似问题
腾讯云开发者
