Software

ACE is an open-source constraint solver developed by Christophe Lecoutre (CRIL) in Java.

BE

B+E is a preprocessor that associates with an input CNF formula an output CNF formula which admits the same number of models.

Be

Belief revision games (BRGs) are concerned with the dynamics of the beliefs of a group of communicating agents.

bn

bn2cnf is a translator associating with an input graphical model (a Bayesian network or a Markov network) an output which consists of a CNF formula and a weight map.

Co

br2cnf compiler is a program for compiling a given CNF belief revision instance into a query-equivalent CNF formula.

Co

cnf2eadt is a compiler associating with an input CNF formula an equivalent representation from the language EADT of (extended) affine decision trees.

Co

bm2cnf is a compiler for turning a given CNF merging instance into a query-equivalent CNF formula.

Co

cn2mddg is a compiler associating with a finite-domain constraint network represented in the XCSP 2.1 format an equivalent representation from the language MDDG of multivalued decomposable decision graphs.

Software

A Belief Aggregation Tool.

Cr

Crusti_g2io is a graph generator following an inner/outer pattern..

dD

d-DNNF-reasoner is a tool for reasoning on d-DNNF representations.

DS

D-Syrup is an original distributed SAT solver based on the portfolio paradigm

Software

d4 is a compiler associating with an input CNF formula an equivalent representation from the language Decision-DNNF.

De

Decdnnf-rs is a tool for manipulating Decision-DNNFs produced by d4

De

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

Ge

tt2bm is a program which can be used both to generate time-tabling instances, and to turn them into distance-based merging instances.

Software

Glucose is based on a new scoring scheme for the clause learning mechanism of so called "Modern" SAT sovlers

Software

Gophersat is a SAT and pseudo-boolean solver written purely in go.

Ji

A Java 9+ command-line arguments parsing library based on annotations

Software

A performance analysis toolkit in python

Mi

This is a tool that use itemset mining to compress CNF boolean formulae using tseitin's encoding.

NA

The main purpose of this solver is to experiment nogood recording (with a clause reasoning engine) in Constraint Programming (CP).

pd

pddl2cnf is a translator associating with a classical planning instance encoded in PDDL and a given horizon an output which consists of a CNF formula.

Pe

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.

pF

pFactory is a C++ library that simplifies the design of multithreaded solvers.

Pr

pmc is a preprocessor associating with an input CNF formula an output CNF formula which is either logically quivalent to the input or has only the same number of models as the input.

Software

PyCSP3 is a Python library that allows to develop declarative models of combinatorial problems under constraints.

Py

PyXAI is a Python library allowing to bring explanations of various forms from classifiers resulting from machine learning techniques

Ru

A library designed to generate test cases in an automatic way using translation rules

ru
  • GPL

runsolver allows to finely control the resources (CPU, memory, ...) used by a solver

SA

SAF is a SAT-based Attractor Finder which computes attractors in biological regulatory networks modelled as asynchronous automata networks.

Sa

SATMiner is a library for searching interesting patterns using constraint programming/SAT backend

SA

Keep up to date with the satisfiability problem

Software

SAT4J is a library of efficient boolean reasoners for the Java platform.

Software

A Constraint-based Quick Abstract Argumentation Solver

Sy

Implements a framework for breaking symmetries in itemset mining problems.

th

The aim of the OpenCycloDB project it is provide open reliable data regarding cyclodextrins to facilitate its use in machine learning approaches.

Th

The SAT Game is a funny representation of the SAT problem.

To

This is an algorithm for enumerating the Top-k models of a CNF propositional formula.

Tr

cn2cnf is a translator associating with an input constraint network (respecting the format XCSP3) a CNF formula.

Software

XCSP3 is a universal format, based on XML, allowing to represent instances of constrained combinatorial problems.