基于SAT的依赖处理的原型。这是一个正在进行中的工作，目前不要期望任何API不会改变。
项目描述
基于SAT的依赖处理的原型。这是一个正在进行中的工作，目前不要期望任何API不会改变。
安装
要安装Python包，请按照以下步骤操作
git clone --recursive https://github.com/enthought/sat-solver cd sat-solver pip install -e .
示例用法
TODO
从CLI使用
要从CLI尝试事情，您需要编写一个场景文件（yaml格式），请参阅simplesat/tests/simple_numpy.yaml以获取一个简单示例。
打印规则
python scripts/print_rules.py simplesat/tests/simple_numpy.yaml
打印操作
python scripts/solve.py simplesat/tests/simple_numpy.yaml
与PHP的composer比较
首先，在您的机器上的某个地方克隆composer
git clone https://github.com/composer/composer
然后，使用scripts/scenario_to_php.py脚本来编写一个PHP文件，该文件将打印给定场景的composer解决方案
python scripts/scenario_to_php.py \
--composer-root <path to composer github checkout> \
simplesat/tests/simple_numpy.yaml \
scripts/print_operations.php.in
这将创建一个scripts/print_operations.php脚本，您可以直接使用php执行
php scripts/print_operations.php
参考文献
Niklas Eén, Niklas Sörensson: 一个可扩展的SAT求解器. SAT 2003
Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik: 布尔可满足性问题求解器中的高效冲突驱动学习. Proc. ICCAD 2001，第279-285页。
Donald Knuth: 计算机程序设计艺术. 第4卷，预 fascicle 6A，第7.2.2.2节。（可满足性）。
关于使用SAT求解器管理包的用途
Fosdem 2008演示： 使用SAT解决包依赖关系. 更多详细信息请参阅SUSE wiki。
0install项目。
Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner: OPIUM: 优化的软件包安装/卸载管理器. ICSE 2007会议论文，第178-188页
simplesat 更新日志
版本 0.9.1
修复了simplesat wheel构建问题（#287）
版本 0.9.0
用GitHub Actions替换travis CI（#281）
为Python 3.11运行测试（#284）
版本 0.8.2
发布于2019年10月8日。
修复了在
constraint_modifiers.py中废弃的convert属性，以符合attrs包的19.2.0版本发布（参见https://www.attrs.org/en/stable/changelog.html）。 (#270)修复了
InvalidConstraint错误信息中的错别字。 (#266)修复了
UndeterminedClausePolicy未建议最佳软件包的错误。 (#268)
内部改进
将支持的attrs最低版本改为17.4.0。 (#270)
版本 0.8.1
发布于2017年3月22日。
错误修复
修复了在升级所有软件包时，如果没有远程候选软件包可用，将无法升级已安装软件包的边缘情况（#261）
修复了解析以数字开头的需求文件的问题（#260）
版本 0.8.0
发布于2017年3月9日。
特性
新升级作业类型，用于将所有已安装软件包更新到最新版本（#253）
新求解器方法
solve_with_hint，为不可满足问题提供更易读的消息（#254）
内部改进
更新运行时依赖约束到最新的okonomiyaki（#252）
版本 0.7.0
发布于2016年8月8日。
特性
添加计算一组仓库中叶子软件包的功能。
版本 0.6.0
发布于2016年7月20日。
特性
添加对发布后版本号的支持（#239）
将软件包和软件包ID迭代添加到Pool（#237）
版本 0.5.0
发布于2016年7月12日。
特性
在检查需求的可满足性/完备性时返回错误信息文本（#231）
为ConstraintModifiers添加
remove方法，用于删除与特定软件包关联的约束（#229）
版本 0.4.0
发布于2016年6月1日。
特性
ConstraintModifiers增强：添加update方法；在Request上的修饰符使用验证器（#211）添加计算一组子句的一些最小不可满足子集的功能（#219）
为
Request添加soft-update作业。对于软更新，策略优先建议较新版本而不是已安装版本（#220）
错误修复
跟踪求解器中只有一个文字的子句，以避免策略中的崩溃（#209）
如果已安装的软件包没有关联的子句，则在策略中避免失败（#218）
版本 0.3.0
发布于2016年5月5日。
特性
添加对
provides元数据的支持（#194）添加简化并满足请求的新API（#195）
增强
更新
install_requires以允许okonomiyaki >= 0.14（#197）Request现在使用
attrs（#196）更新有关各种需求类型的内部文档（#201）
错误修复
修复了当使用
Repository.find_packages查找不存在软件包时，在Repository.add_package中出现的错误（#185）修复了元数据冲突时的错误处理（#187）
修复了需求中的软件包名解析（#193）
调用
asdict必须是确定的（#200）
版本 0.2.2
发布于2016年4月29日。
更新
install_requires以允许okonomiyaki >= 0.14（#198）
版本 0.2.1
发布于2016年4月27日。
修复了当使用
Repository.find_packages查找不存在软件包时，在Repository.add_package中出现的错误（#185）修复了元数据冲突时的错误处理（#187）
版本 0.2.0
增强
与不可满足场景相关的详细信息记录在
UNSAT对象中，并附加到引发的SatisifiabilityError上（#101）。sat solver不再依赖于enstaller，并且除了okonomiyaki之外，仅使用非Enthought库（#127、#114、#113、#111、#110、#109、#107、#105）
支持对依赖性要求的临时放宽（#140）
添加了文档
处理包含对不存在要求的引用的包元数据的情形。现在默认忽略这些引用，而不是使求解器崩溃（#156）。
向satsolver添加了__version__和__git_revision__属性（#173）。
已修复的错误
IPolicy构造函数现在忽略初始化参数（#101）。
已修复了一些使用非唯一键的排序操作（#101）。
假设现在表示为一个空的子句对象（#101）。
对分布名称和版本解析更加严格（#146）。
清理设置，在setup.py中添加了缺少的enum34作为依赖项（#169，#170）。
内部改进
内部API用于检查一组要求的一致性（#157）。
修复了scripts/solve.py中的调试输出（#159）。
添加了一个实用脚本，用于将场景导出到DIMACS格式（#162）。
内部API用于计算要求的逆向依赖（#175）。
版本 0.1.0
这是simplesat的初始版本。虽然SAT求解器功能齐全，但构建要解决的子句集的基础设施支持使用仅等于约束指定的运行时依赖项，例如numpy 1.8.0-1 depends MKL ^= 10.3。
特性
提供MiniSAT的纯Python实现，支持通过插件式Policy对象进行定向搜索。
读取和解决基于yaml的场景描述。这些可以可选地指定以下内容
可用的软件包
当前安装的软件包
“标记”的软件包，这些软件包必须在有效解决方案中存在
任何数量的请求的面向软件包的操作
安装
删除
更新
全部更新
预期的解决方案作为此类软件包操作列表
预期无法解决的场景的失败信息。
在搜索过程中记录关于值分配和假设的详细信息。
努力从解决方案中修剪不相关的真值，即找到解决问题所需的最小值集。
下载文件
下载您平台的文件。如果您不确定选择哪个，请了解有关安装软件包的更多信息。