Software
  • LGPL

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

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.

Wo

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

YA

YAHSP is a Heuristic Search Planner