The solver for the Touist language

| Mac, Linux | Windows | Reference manual | Come and discuss! |
| | | | |


  1. TouIST has a java-based graphical interface (which embeds the
    command-line tool). It be downloaded in the releases page and is available
    for Linux, Windows and macOS. Two options are available: the plain jar
    for any platform or the non-signed native version for macOS and
    Windows (see below warning).

    ⚠ WARNING ⚠ On macOS Sierra, the native will show a
    broken message. You must run sudo spctl --master-disable which will
    enable the Open apps from anywhere.

    ⚠ WARNING ⚠ On Windows 10, the native TouIST.exe can't be opened unless
    the Windows Defender SmartScreen feature is disabled. You can still use
    the jar version.

  2. If you only want the command-line program touist, it can be installed
    using either brew (linux/mac)
    or opam.

    Using brew (recommended, provides pre-built binaries):

    brew install touist/touist/touist          # stable version
    brew install touist/touist/touist --HEAD   # git-master version

    Using opam (yices2 and qbf are optionnal, you can skip them if
    you don't need the embedded SMT/QBF solvers):

    opam install yices2 qbf touist          # stable version
    opam pin add touist --dev-repo          # git-master version

    Now, if we want to know if a ⋀ b ⇒ c is satisfiable:

    echo 'a and b => c' | touist - --solve

    The manual (man touist or touist --help) comes very handy, take a look
    at it!

    To build touist from source, see src/

  1. You can also look at the TouIST reference manual
    (pdf version).

  2. Syntax coloring is also available for VSCode (search
    for the touist extension) and for Vim (Vim support is experimental).


TouIST is a user-friendly tool for solving propositional logic problems using
a high-level logic language (known as the bigand format or syntax or
language). This language allows complex expressions like big and, sets...

We can for example solve the problem "Wolf, Sheep, Cabbage", or a sudoku, or
any problem that can be expressed in propositional logic.

The TouIST has been initialized by Frederic Maris and Olivier Gasquet,
associate professors at the Institut de Recherche en Informatique de Toulouse
(IRIT). It is a "second" or "new" version of a previous program,

The development is done by a team of five students1 in first year of master's
degree at the Université Toulouse III — Paul Sabatier. This project is a part
of their work at school.

What is Touist made of?

  1. the main program, touist, is written in OCaml and is compiled
    into a native and standalone binary. It does the parsing, the transformations
    (e.g., latex) and embeds one solver per theory (SAT, SMT and QBF) in order
    to solve the problem.

  2. the java-based graphical interface uses Java (>= jre7) and Swing; it embeds
    a copy of the touist binary.

Here is a small figure showing the architecture of the whole thing:


See the ./ file.

Tested architectures

| | GNU/Linux, BSD | Windows | macOS |
| ---------------------- | -------------- | ---------------------- | ----- |
| touist (opam) | yes | yes (mingw32+mingw64) | yes |
| qbf (opam) | yes | yes (minw32 only [^1]) | yes |
| yices2 (opam) [^2] | yes | no | yes |
| yices2 (source) [^2] | yes | yes (mingw32+mingw64) | yes |

[^1]: the qbf package only works on mingw32 because of a slight bug in the
./configure of quantor-3.2. See maelvalais's PR on the ocaml-qbf repo.

[^2]: yices2 needs the gmp library on the system. On linux and macos, opam
will install it for you using the command opam depext conf-gmp.


You can also use the touist library; it is installed using
opam install touist and requires the version 3.4.0 or above.
The API reference is here. For example, in utop:

#require "touist";;
open Touist;;
"a and b and c"
    |> Parse.parse_sat
    |> Eval.eval
    |> Cnf.ast_to_cnf
    |> SatSolve.minisat_clauses_of_cnf
    |> SatSolve.solve_clauses
        ~print:(fun tbl model _ -> SatSolve.Model.pprint tbl model |> print_endline);;

will return

1 c
1 b
1 a
- : SatSolve.ModelSet.t = <abstr>

The API is kind of spread among many modules (which could be gathered in one
single module), sorry for that! We really hope to have some time to
put everything in a nice module well organized.

Bugs and feature requests

You can report bugs by creating a new Github issue. Feature requests can also
be submitted using the issue system.

You can contribute to the project by forking/pull-requesting.


  1. Olivier Gasquet, Andreas Herzig, Dominique Longin, Frédéric Maris, and
    Maël Valais. TouIST Again… (Formalisez et Résolvez Facilement Des
    Problèmes Avec Des Solveurs SAT, SMT et QBF).
    In Actes Des 10es
    Journées d’Intelligence Artificielle Fondamentale (IAF 2017). 2017.

  2. Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba,
    Olivier Lezaud, Frédéric Maris, and Maël Valais La Logique Facile Avec
    TouIST (formalisez et Résolvez Facilement Des Problèmes Du Monde Réel
    . In Actes Des 9es Journées d’Intelligence Artificielle
    Fondamentale (IAF 2015). 2015.

  3. Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba,
    Olivier Lezaud, Frederic Maris, and Mael Valais. Twist Your Logic with
    . CoRR abs/1507.03663. 2015.

  4. Gasquet O., Schwarzentruber F., Strecker M. Satoulouse: The Computational
    Power of Propositional Logic Shown to Beginners
    . In:
    Blackburn P., van Ditmarsch H., Manzano M., Soler-Toscano F. (eds) Tools
    for Teaching Logic. Lecture Notes in Computer Science, vol 6680. Springer,
    Berlin, Heidelberg. 2011.

with-test & < "2.2.6"
>= "0.9.8"
>= "20151023"
>= "1.0+beta12"
>= "4.02.3"
Reverse Dependencies