  SAT provers are powerful tools for solving real-sized logic problems, but
using them requires solid programming knowledge and may be seen w.r.t.\ logic
like assembly language w.r.t.\ programming. Something like a high level
language was missing to ease various users to take benefit of these tools. {\sc
\texttt {TouIST}}\ aims at filling this gap. It is devoted to propositional
logic and its main features are 1) to offer a high-level logic langage for
expressing succintly complex formulas (e.g.\ formulas describing Sudoku rules,
planification problems,\ldots) and 2) to find models to these formulas by using
the adequate powerful prover, which the user has no need to know about. It
consists in a friendly interface that offers several syntactic facilities and
which is connected with some sufficiently powerful provers allowing to
automatically solve big instances of difficult problems (such as time-tables or
Sudokus). It can interact with various provers: pure SAT solver but also SMT
provers (SAT modulo theories - like linear theory of reals, etc) and thus may
also be used by beginners for experiencing with pure propositional problems up
to graduate students or even researchers for solving planification problems
involving big sets of fluents and numerical constraints on them.
