CSP2SAT: Compiling Finite Linear CSP into SAT

Overview

CSP2SAT solves Finite Linear CSPs (Constraint Satisfaction Problems) and Finite Linear COPs (Constraint Optimization Problems) by encoding them into SAT (Boolean Satisfiability Testing) Problems.

The encoding method used in this program is called Order Encoding which assigns a boolean variables p_xi meaning x <= i for each integer variable x and integer constant i.

There are other CSP2SAT programs: csp2sat by Olivier Roussel and CSP2SAT by Helene Fargier. They are independently developed and older than this system.

Download

• Sugar is a new and faster version written in Java (it works with an external SAT solver, such as MiniSat). It is recommended to use Sugar instead of CSP2SAT.
• csp2sat_v03.zip
  • Requirements: MiniSAT, Perl
• CSP instances
  • Open-Shop Scheduling Problems: oss.zip
  • Job-Shop Scheduling Problems: jss.zip
  • Graph Coloring Problems: gcp.zip

Benchmark Results

• Open-Shop Scheduling Problems
• Job-Shop Scheduling Problems
• Graph Coloring Problems

Publications

• See Technical Papers and Presentation Slides section of Sugar: A SAT-based Constraint Solver page.

Related Projects

• Cream: Class Library for Constraint Programming in Java
• HECS

Links

• MiniSat v1.14
• International CSP Solver Competition
  • First International CSP Solver Competition
  • Second International CSP Solver Competition (Benchmarks, Results)

License

CSP2SAT (Compiling Finite Linear CSP into SAT)
Copyright (C) 2006 by Naoyuki Tamura (tamura @ kobe-u.ac.jp)

CSP2SAT is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

CSP2SAT is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.