文件名称：azucar-solver:糖
文件大小：272KB
文件格式：ZIP
更新时间：2024-07-08 13:45:12
Java
Azucar：基于“紧凑顺序编码”的基于SAT的CSP求解器 Azucar 是基于 SAT 的 CSP 求解器，它是的增强版本， 是 2008 年和 2009 年国际 CSP 求解器竞赛的 GLOBAL 类别获奖系统。 它可以解决整数上的有限非线性约束满足问题 (CSP)、约束优化问题 (COP) 和 Max-CSP。 Azucar 使用一种新的 SAT 编码方法，称为紧凑顺序编码。 在紧序编码中，每个整数都用任意基数的数字系统表示，每个数字比较都用序编码进行编码。 在顺序编码中，对于每个整数变量x和整数值a ，比较x <= a由不同的布尔变量编码。