SAT解算工具的接口（如miniSAT）
satisp的Python项目详细描述
satispy是一个python库，旨在成为各种 SAT（布尔可满足性）求解应用程序。
支持的解算器：
- [MiniSAT](http://minisat.se/) (Linux)
- [Lingeling](http://fmv.jku.at/lingeling/) (Linux, Cygwin)
对其他偿付方的支持应该相当容易，只要他们接受 [dimacs cnf sat格式]（http://www.satcompetition.org/2009/format-benchmarks2009.html）。
安装
您可以从pypi获取当前版本：
$ sudo pip install satispy
或者可以从https://github.com/netom/satispy下载副本，然后 运行
$ sudo ./setup.py install
在项目的目录中。
如果要在库上开发，请使用：
$ ./setup.py develop
您可以通过运行run_tests.py来运行在测试文件夹中找到的测试。
工作原理
你需要一个SAT解算器和numpy来安装在你的机器上。
让我们看一个例子：
from satispy import Variable, Cnf from satispy.solver import Minisat
v1 = Variable(‘v1’) v2 = Variable(‘v2’) v3 = Variable(‘v3’)
exp = v1 & v2 | v3
solver = Minisat()
solution = solver.solve(exp)
- if solution.success:
- print “Found a solution:” print v1, solution[v1] print v2, solution[v2] print v3, solution[v3]
- else:
- print “The expression cannot be satisfied”
这个程序试图满足布尔表达式
v1&v2 v3
你可以通过给所有变量赋值true来实现，例如， 但也有其他的解决办法。这个程序发现一个任意的 解决方案。
首先，程序导入不同的类，这样我们就可以构建一个表达式 试着解决它。
每个表达式都是cnf形式的，但我们不必输入表达式 在里面。cnf类负责布尔值的正确排列。 条款。
表达式可以通过创建变量并将它们粘在一起来构建 任意使用布尔运算符：
- 不是：-（一元）
- 以及：&；
- 或：
- 异或：^
- 含义>>
求解类ministat用于求解公式。
注意：minist类创建两个临时文件，因此需要写入 访问系统的临时目录
可以通过读取“success”布尔值来检查返回的解决方案 旗帜。
然后，可以使用该解决方案查询变量分配 就像一本字典。请注意，使用的是变量对象，而不是字符串。
（这个示例可以在examples目录中找到）
欢迎加入QQ群-->： 979659372
