Compiling finite linear CSP into SAT
Compiling finite linear CSP into SAT
复制标题
DOI：
10.1007/s10601-008-9061-0
复制
发表时间：
2009-06-01
期刊：
影响因子：
1.6
通讯作者：
Banbara, Mutsunori
中科院分区：
文献类型：
--
作者：
Tamura, Naoyuki;Taga, Akiko;Banbara, Mutsunori
本文提出了一种将整数线性约束的约束满足问题(CSP)和约束优化问题(COP)编码为布尔可满足性测试问题(SAT)的新方法。这种编码方法(命名为Order Coding)与Crawford和Baker用于对作业车间调度问题进行编码的方法基本相同。比较千分之x表示欧元千分之a由每个整数变量x和整数值a的不同布尔变量编码。为了评估该方法的有效性，我们将该方法应用于Open-Shop调度问题(OSS)。对三个OSS基准测试集的192个实例进行了测试，发现并证明了所有实例的最优结果，其中包括三个先前未确定的问题。
In this paper, we propose a new method to encode Constraint Satisfaction Problems (CSP) and Constraint Optimization Problems (COP) with integer linear constraints into Boolean Satisfiability Testing Problems (SAT). The encoding method (named order encoding) is basically the same as the one used to encode Job-Shop Scheduling Problems by Crawford and Baker. Comparison x a parts per thousand currency signaEuro parts per thousand a is encoded by a different Boolean variable for each integer variable x and integer value a. To evaluate the effectiveness of this approach, we applied the method to the Open-Shop Scheduling Problems (OSS). All 192 instances in three OSS benchmark sets are examined, and our program found and proved the optimal results for all instances including three previously undecided problems.