FznTini

FznTini is a general constraint solver purely based on SAT. It solves constraint satisfaction and optimization problems written in FlatZinc (not involving floating point numbers) via Booleanization and calls to the Tinisat SAT solver. It can also print Booleanizations of constraint models in DIMACS CNF, to be solved by independent SAT solvers. Constraint modeling languages that have translations to FlatZinc, such as MiniZinc, are automatically supported as well.

FznTini is described in Universal Booleanization of Constraint Models, Jinbo Huang, Proceedings of the 14th International Conference on Principles and Practice of Constraint Programming (CP-08).

You can download a Linux executable of FznTini and an example FlatZinc file modeling a job shop scheduling problem. More examples are available in the G12 MiniZinc Distribution.

(Note that the Zinc family of languages have changed since the completion of the work described in the above paper. The FznTini executable provided here supports MiniZinc Distribution Version 0.8 or later.)

Back to my home page.