package touist

  1. Overview
  2. Docs

Description

The Touist language is a friendly language for writing propositional logic (SAT), logic on real and integers (SMT) and quantified boolean formulas (QBF). This language aims to formalize real-life problems (e.g., the sudoku can be solved in a few lines). Touist embeds a SAT solver (minisat) and can be built with optionnal SMT and QBF solvers. Touist is also able to generate the latex, DIMACS, SMT-LIB and QDIMACS formats from a touist file.

Optionnal solvers:

  • for using Yices2 (--smt --solve), run opam install yices2
  • for using Quantor (--qbf --solve), run opam install qbf

Published: 09 Dec 2017

README

TouIST, the language for propositional logic

Mac, Linux Windows Reference manual Come and discuss!
trv-img apvy-img cir-img gitter-img

Install

  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 TouIST.app 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/HOWTODEBUG.md.

  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).

Description

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, SAToulouse.

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:

Rebuilding-it

See the ./INSTALL.md 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.

TouIST API

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.

References

  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 TouIST. 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.

Dependencies (6)

  1. cmdliner >= "0.9.8"
  2. re
  3. minisat < "0.6"
  4. menhir >= "20151023"
  5. jbuilder >= "1.0+beta12"
  6. ocaml >= "4.02.3"

Dev Dependencies (2)

  1. odoc with-doc
  2. ounit with-test & < "2.2.6"

Used by

None

Conflicts (2)

  1. yices2 < "0.0.2"
  2. qbf < "0.1"