• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Tools with Artificial Intelligence >Compiling Pseudo-Boolean Constraints to SAT with Order Encoding
【24h】

Compiling Pseudo-Boolean Constraints to SAT with Order Encoding

机译：使用订单编码将伪布尔约束编译为SAT

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper presents a SAT-based pseudo-Boolean (PB for short) solver named PBSugar. PBSugar translates a PB instance to a SAT instance by using the order encoding, andsearches its solution by using an external SAT solver, such as Glucose. We first introduce an optimized version of the order encoding, and it is appliedto encode each PB constraint a1 x1 +...an xn # k. The encoding isreformulated as a sparse Boolean matrix, named Counter Matrix, of size n × (k+1) constructed for each PB constraint. The same Counter Matrix can be usedfor any relations ≥, ≤, =, and ≠, and can be reused for other PBconstraints having common sub-terms. The experimental results for 669 instances of DEC-SMALLINT-LIN category(decision problems, small integers, linear constraints) demonstrates thesuperior performance of PBSugar compared to other state-of-the-art PB solvers interms of the number of solved instances within the given time limit.
机译：本文提出了一种基于SAT的伪布尔（简称PB）求解器PBSugar。 PBSugar使用顺序编码将PB实例转换为SAT实例，并使用外部SAT求解器（例如葡萄糖）搜索其解。我们首先介绍顺序编码的优化版本，并将其应用于对每个PB约束a1 x1 + ... an x​​n＃k进行编码。编码被重新构造为为每个PB约束构造的大小为n×（k + 1）的稀疏布尔矩阵，称为计数器矩阵。相同的Counter Matrix可以用于≥，≤，=和≠的任何关系，并且可以重用于具有公共子项的其他PB约束。针对DEC-SMALLINT-LIN类别的669个实例（决策问题，小整数，线性约束）的实验结果证明，在给定范围内，已解决实例的数量方面，PBSugar与其他最新的PB求解器相比具有优越的性能时限。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号