Kodkod
=======

This repository includes the source code for the
[Kodkod](http://alloy.mit.edu/kodkod/index.html) solver for relational
logic.  Kodkod provides a clean Java [API](http://alloy.mit.edu/kodkod/release/doc/) for constructing,
manipulating, and solving relational constraints. The
source code is extensively documented, and the repository includes
many [examples](https://github.com/emina/kodkod/tree/master/examples/kodkod/examples) demonstrating the use of the Kodkod API.

Kodkod is open-source and available under the [MIT license](LICENSE). However, the implementation relies on third-party SAT solvers ([SAT4J](http://www.sat4j.org), [MiniSat](http://minisat.se), [Glucose](http://www.labri.fr/perso/lsimon/glucose/), and [(P)Lingeling](http://fmv.jku.at/lingeling/)), some of which are released under stricter licenses. Please see the solver licenses for details.  

	
NOTE: Kodkod will pickup plingeling (as well as its native libraries) when needed from a path given via -Djava.library.path=... or, if not found there, it will look it up via the PATH environment variable. As usual first match wins.


You may run the  [Sudoku example](https://github.com/emina/kodkod/blob/master/examples/kodkod/examples/sudoku/Sudoku.java) as follows:

  `$ java -cp kodkod.jar:examples.jar -Djava.library.path=. kodkod.examples.sudoku.Sudoku`  
  
The program will produce a solution to a sample Sudoku puzzle:

```
p cnf 3452 7954
primary variables: 486
translation time: 176 ms
solving time: 2 ms
+-------+-------+-------+
| 6 4 7 | 2 1 3 | 9 5 8 | 
| 9 1 8 | 5 6 4 | 7 2 3 | 
| 2 5 3 | 8 7 9 | 4 6 1 | 
+-------+-------+-------+
| 1 9 5 | 6 4 7 | 8 3 2 | 
| 4 8 2 | 3 5 1 | 6 7 9 | 
| 7 3 6 | 9 2 8 | 1 4 5 | 
+-------+-------+-------+
| 5 7 4 | 1 9 2 | 3 8 6 | 
| 8 2 9 | 7 3 6 | 5 1 4 | 
| 3 6 1 | 4 8 5 | 2 9 7 | 
+-------+-------+-------+
```