基于pybind11的葡萄糖sat解算器结合
pyglucose的Python项目详细描述
葡萄糖
pybind11基于glucose SAT solver的绑定。
安装
pip install git+https://github.com/msakai/glucose-pybind11/
基本用法
pyglucose模块导出Solver和Lit
SAT问题的解决方法如下：
- 使用
solver = Solver()构造解算器实例。 - 使用
var = solver.new_var()分配变量。 变量作为整数值返回，并且可以通过Lit(var)转换为Lit。 文本lit可以被取反为~lit。 - 使用
solver.add_clause(clause)添加子句子句表示为Iterable[Lit]。 - 使用
solver.solve()解决问题 - 如果
solver.okay属性是True，那么问题是SATISFIABLE，并且 可以使用solver.model属性检索满意的赋值。 否则，问题是UNSATISFIABLE
许可证
欢迎加入QQ群-->： 979659372
