CRIL members have developed tools and prototypes that are available to the scientific community.

CSP & SAT Solvers

  • Abscon
    Abscon 109 is the solver that has been submitted to the (second round of the) 2006 Competition of CSP solvers.
  • Glucose
    Glucose is based on a new scoring scheme for the clause learning mechanism of so called "Modern" SAT sovlers
  • ManySat
    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
  • PeneLoPe
    PeneLoPe, a parallel SAT solver
  • ReViVal
    ReViVal is a simplification technique of CNF formulas developed by Cédric Piette, Youssef Hamadi and Lakhdar Saïs.
  • SAT4J : the satisfiability library for Java
    SAT4J is a library of efficient SAT solvers for the Java platform.
  • ppfolio
    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.

Reasoning

Compilers

  • The Compile! Project
    The Compile! Project gathers the research done at CRIL about knowledge compilation.

Declarative Mining

  • DecMining
    DecMining is a web page dedicated to declarative approaches for data mining. It contains software, datasets, publications and related links to others research groups.

Game Solver

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

Other

  • Alloy 4 Eclipse
    Allo4eclipse (A4E) plugin allows the specification and analysis of models in the Alloy4 language on the Eclipse platform.
  • Personalised Museum Visits
    Ask yourself about what you would be doing if you just have one hour and a half to spend at Le Louvre? Our purpose is to help a visitor finding a “good answer” to such a question.
  • runsolver
    runsolver allows to finely control the resources (CPU, memory, ...) used by a solver

Web sites

  • SAT Live!
    Keep up to date with the satisfiability problem
  • The SAT Game
    The SAT Game is a funny representation of the SAT problem.
  • XCSP
    XCSP3 is a XML-based format designed to represent combinatorial constrained problems.

Older software