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 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 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.