July 4th, 2018: on macOS, TouIST.jar only works with Java <= 8 (cf. issue). I am working on a fix. For now, the workaround is to use Java 8 😕.
🔰 Reference manual |
New: you can start hacking with touist
using Gitpod; to start the
online editor with the touist project open, click
here! Once there,
dune build
to rebuild and touist
to test touist.
-
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 runsudo 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. -
If you only want the command-line program
touist
, it can be installed using eitherbrew
(linux/mac) oropam
.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
andqbf
are optionnal, you can skip them if you don't need the embedded SMT/QBF solvers):opam install yices2 qbf touist opam pin add touist --dev-repo # git-master version
Now, if we want to know if
a ⋀ b ⇒ c
is satisfiable:touist - --solve <<< "a and b => c"
where
-
tells touist to expect a formula on stdin and<<<
gives the right-hand string to stdin.The manual (
man touist
ortouist --help
) comes very handy, take a look at it!To build
touist
from source, seesrc/HOWTODEBUG.md
. -
You can also look at the TouIST reference manual (pdf version).
-
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, 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.
-
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. -
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 ./INSTALL.md file for building from source.
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 |
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.
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.
-
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.
-
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.
-
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.
-
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.