CSP2SAT: Compiling Finite Linear CSP into SAT


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


Benchmark Results


Related Projects



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.

Naoyuki Tamura