Home

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


    \[\bigwedge_{ i \in { 1 .. 9 } }\bigvee_{ j \in { 1 .. 9 } }\bigwedge_{ n \in { 1 .. 9 } }\bigwedge_{\substack{ m \in { 1 .. 9 }\\ m \neq n }}(p_{i, j, n} \rightarrow \neg p_{i, j, m} )\]

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

We can conveniently express and solve problems such as the Sudoku (see example) or finding a winning strategy for the Nim game (Gasquet et al. [3], example).

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.

Also, feel free to come to our Gitter chatroom for any request, bug or remarks! Or you can create a ticket on the issue tracker.