Compiling finite linear CSP into SAT |
| |
Authors: | Naoyuki Tamura Akiko Taga Satoshi Kitagawa Mutsunori Banbara |
| |
Affiliation: | (1) Information Science and Technology Center, Kobe University, Kobe, Japan;(2) Graduate School of Science and Technology, Kobe University, Kobe, Japan |
| |
Abstract: | 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 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. |
| |
Keywords: | Constraint satisfaction problems SAT encoding Open-shop scheduling problems |
本文献已被 SpringerLink 等数据库收录! |
|