Software

The laboratory tries as much as possible to make the software it produces available as free software. These software are identified by a badge that mentions their free license.

The use of a free license aims at facilitating the diffusion of our research results in the academic world and more generally in our digital society. It is also a way for the laboratory to share the effort of maintaining the tools and libraries it develops for its internal needs. These software are often available “in open development”, on the laboratory’s github account.

Software
  • LGPL

Allo4eclipse (A4E) plugin allows the specification and analysis of models in the Alloy4 language on the Eclipse platform.

Software

A Constraint-based Quick Abstract Argumentation Solver

CP

CPT is a temporal planner.

LS

The LSAT solver was classified second during the international SAT’03 competition (category : "hand-made").

Ma

ManySat is a DPLL-engine which includes all the classical features like two- watched-literal, unit propagation, activity-based decision heuristics, lemma dele- tion strategies, and clause learning

Op

OpenQBF is a QBF solver written in Java. It is simple but correct. It is not maintained anymore since 2004. Source code is available at sourceforge.

Pe

PeneLoPe, a parallel SAT solver

pp
  • GPL

ppfolio (Pico PortFOLIO or also Parallel PortFOLIO) is a very naive parallel portfolio. It is meant to identify a lower bound of what can be achieved either with portfolios, or with parallel solvers.

PR
  • GPL

PRISM stands for Platform for Reasoning with Inconsistency Shapley Measure.

QB

QBFL is a QBF solver taking advantage of the polynomial classes of this problem.

Re

ReViVal is a simplification technique of CNF formulas.

va

Wo

WoodStock is a constraint-based general game player for the General Game Playing (GGP).

YA

YAHSP is a Heuristic Search Planner