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. Examples problems in MiniZinc and the MiniZinc-to-FlatZinc translator 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 FlatZinc 1.1.)

Back to my home page