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

Perennial software

These software are written and maintained on the long term by permanent members of the CRIL.

  • AbsCon
    AbsCon 109 is the solver that has been submitted to the (second round of the) 2006 Competition of CSP solvers.
  • COmputer SCIeNce pUblication Statistics
  • Glucose MIT
    Glucose is based on a new scoring scheme for the clause learning mechanism of so called "Modern" SAT sovlers
  • SAT4J, the satisfiability library for Java EPLLGPL
    SAT4J is a library of efficient boolean reasoners for the Java platform.
  • XCSP
    XCSP3 is a XML-based format designed to represent combinatorial constrained problems.
  • runsolver GPL
    runsolver allows to finely control the resources (CPU, memory, ...) used by a solver

Recent software

  • CoQuiAAS GPL
    A Constraint-based Quick Abstract Argumentation Solver
  • Gophersat MIT
    Gophersat is a SAT and pseudo-boolean solver written purely in go.
  • Jigsaw-CLI GPL
    A Java 9+ command-line arguments parsing library based on annotations
  • NACRE GPL
    The main purpose of this solver is to experiment nogood recording (with a clause reasoning engine) in Constraint Programming (CP).
  • Rubens GPL
    A library designed to generate test cases in an automatic way using translation rules
  • d4
    d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF.
  • pFactory, a library for multithreaded SAT solvers GPL
    pFactory is a C++ library that simplifies the design of multithreaded solvers.

CSP & SAT Solvers

  • AbsCon
    AbsCon 109 is the solver that has been submitted to the (second round of the) 2006 Competition of CSP solvers.
  • AmPharoS
    A distributed SAT solver based on the divide and conquer paradigm
  • D-Syrup
    D-Syrup is an distributed SAT solver based on the portfolio paradigm
  • Glucose MIT
    Glucose is based on a new scoring scheme for the clause learning mechanism of so called "Modern" SAT sovlers
  • Gophersat MIT
    Gophersat is a SAT and pseudo-boolean solver written purely in go.
  • 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
  • NACRE GPL
    The main purpose of this solver is to experiment nogood recording (with a clause reasoning engine) in Constraint Programming (CP).
  • PeneLoPe
    PeneLoPe, a parallel SAT solver
  • ReViVal
    ReViVal is a simplification technique of CNF formulas.
  • SAT4J, the satisfiability library for Java EPLLGPL
    SAT4J is a library of efficient boolean reasoners for the Java platform.
  • pFactory, a library for multithreaded SAT solvers GPL
    pFactory is a C++ library that simplifies the design of multithreaded solvers.
  • ppfolio 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.

Reasoning

Compilers

  • The Compile! Project
    The Compile! Project gathers the research done at CRIL about knowledge compilation.
  • d4
    d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF.

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.
  • Jigsaw-CLI GPL 
    A Java 9+ command-line arguments parsing library based on annotations
  • 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.
  • Rubens GPL 
    A library designed to generate test cases in an automatic way using translation rules
  • runsolver GPL 
    runsolver allows to finely control the resources (CPU, memory, ...) used by a solver

Web sites

Older software