# 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

## Publications

## Related Projects

## Links

- MiniSat v1.14
- International CSP Solver Competition

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

Naoyuki Tamura
(
Last modified: Sat Aug 20 09:50:09 2011 JST
,
Since Jan 1, 2007
)