没有项目描述
pycscl的Python项目详细描述
Pycscl 0.2.0
python 3的cutesatconstraint编码器库l
pycscl是命题逻辑约束编码器的集合。你可以用它 例如，减少 NP-complete problems到实例 的 Boolean satisifability (SAT) problem， 得益于强大的现成SAT 求解者。
尽管PycSL的设计不依赖于特定的SAT解算器接口， 它包含一个简单易用的绑定 SAT解算器实现 IPASIR接口。
pycscl的版本控制方案是Semantic Versioning 2.0.0。
安装pycscl
先决条件
pycscl除了python 3.7之外没有任何依赖项。
发布包
pycscl版本分布在Python Package Index上。
为了与包命名约定保持一致，pycscl包被命名为pycscl。
要安装最新的pycscl发布包，只需使用pip：
python3 -m pip install pycscl
定制套餐
或者，您可以签出这个存储库并安装pycscl 自己创建一个包。导航到pycscl目录并发出命令
python3 setup.py sdist
这将在
目录dist。现在，您可以安装自定义pycscl包
通过运行
python3 -m pip install <PathToPyCSCL>/dist/pycscl-<Version>.tar.gz
文档
编码器
基数（最多k个）约束编码器
- 二项式编码
- ltseq编码
- 指挥官编码
包装：cscl.cardinality_constraint_encoders
门约束编码器
- 和或二进制异或门
- 二进制mux门
- 半加器和全加器门
包装：cscl.basic_gate_encoders
位矢量约束编码器
- 位向量和或异或门
- 波纹进位矢量加法器和（2的补码）减法门
- 并行位矢量乘法器门
- 无符号位矢量除法器和模门
- 有符号（2补码）和无符号位向量比较门
包装：cscl.bitvector_gate_encoders
示例
cscl_examples.factorization：integer factorization问题编码器cscl_examples.sudoku：基于sat的{a9}求解器cscl_examples.smt_qfbv_solver（在建）：简单qf-bv SMT求解器
欢迎加入QQ群-->： 979659372
