Repository files navigation

July 4th, 2018: onmacOS, TouIST.jar only works with Java <= 8 (cf.issue).I am working ona fix. For now, the workaround is to use Java 8 😕.

New: you can start hacking withtouist usingGitpod; to start theonline editor with the touist project open,clickhere! Once there,dune build to rebuild andtouist to test touist.

1. TouIST has a java-based graphical interface (which embeds thecommand-line tool). It be downloaded in thereleases page and is availablefor Linux, Windows and macOS. Two options are available: the plainjarfor any platform or the non-signednative version for macOS andWindows (see below warning).

   ⚠ WARNING ⚠ On macOS Sierra, the nativeTouIST.app will show abroken message. You must runsudo spctl --master-disable which willenable theOpen apps from anywhere.

   ⚠ WARNING ⚠ On Windows 10, the nativeTouIST.exe can't be opened unlesstheWindows Defender SmartScreen feature is disabled. You can still usethejar version.

2. If you only want the command-line programtouist, it can be installedusing eitherbrew (linux/mac)oropam.

   Usingbrew (recommended, provides pre-built binaries):

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

   Usingopam (yices2 andqbf are optionnal, you can skip them ifyou don't need the embedded SMT/QBF solvers):

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

   Now, if we want to know ifa ⋀ 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 alook at it!

   To buildtouist from source, seesrc/HOWTODEBUG.md.

3. You can also look at theTouIST reference manual(pdf version).

4. Syntax coloring is also available forVSCode (searchfor thetouist extension) and forVim (Vim support is experimental).

   

TouIST is a user-friendly tool for solving propositional logic problems usinga high-level logic language (known as thebigand format or syntax orlanguage). This language allows complex expressions likebig and,sets...

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

The TouIST has been initialized by Frederic Maris and Olivier Gasquet,associate professors at theInstitut 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'sdegree at theUniversité Toulouse III — Paul Sabatier. This project is a partof their work at school.

1. the main program,touist, is written in OCaml and is compiledinto 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 orderto solve the problem.

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

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

See the./INSTALL.md file for building from source.

You can also use thetouist library; it is installed usingopam install touist and requires the version 3.4.0 or above. The API reference ishere. For example, inutop:

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

will return

1 c1 b1 a- : SatSolve.ModelSet.t = <abstr>

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

You can report bugs by creating a new Github issue. Feature requests canalso be submitted using the issue system. You can contribute to the projectby forking/pull-requesting.

1. Olivier Gasquet, Andreas Herzig, Dominique Longin, Frédéric Maris, andMaël Valais.TouIST Again… (Formalisez et Résolvez Facilement DesProblèmes Avec Des Solveurs SAT, SMT et QBF). In Actes Des 10esJourné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 ValaisLa Logique Facile AvecTouIST (formalisez et Résolvez Facilement Des Problèmes Du Monde Réel). In Actes Des 9es Journées d’Intelligence ArtificielleFondamentale (IAF 2015). 2015.

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

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