View Related Documents

Abstract

In this paper, we propose a 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 is basically the same with the one used to encode Job-Shop Scheduling Problems by Crawford and Baker. Comparison xa 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 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.

Fulltext Preview

Image of the first page of the fulltext document