TouIST (Toulouse Integrated Satisfiability Tool) makes it possible to encode any problem formulated in propositional logic (with variants like QBF or by adding integer or floating point constraints) using a powerful language integrating connectors allowing quantification on finite sets.
Beyond the Boolean connectives of propositional logic, the input language of TouIST allows sets, conjunctions and disjunctions parametrized by sets, abbreviations… You can express complex propositional formulas as
which can be written:
bigand $i in [1..9]: bigor $j in [1..9]: bigand $n,$m in [1..9],[1..9] when $m != $n: p($i,$j,$n) => not p($i,$j,$m) end end end
The team behind TouIST consists of Olivier Gasquet, Dominique Longin and Frédéric Maris at Institut de Recherche en Informatique de Toulouse (IRIT). It is a “second” or “new” version of a previous program, SAToulouse. TouIST is still actively developed in ADRIA and LILaC teams.