System CaDiCaL

CaDiCaL

People

Armin Biere, Katalin Fazekas, Mathias Fleury, Nils Froleyks, Florian Pollitt,

Short Description

CaDiCaL is the most advanced incremental SAT solvers. It is not the fastest non-incremental solver (that would go to Kissat according to the SAT competition, partly due to using less memory at the cost of reducing the amount of memory), but it is still very fast and very advanced.

Capabilities

• Proving
• Model finding

Input Language

The input format is simply Dimacs for CNF files

Output

There are two ways to interact: Either non-incrementally by looking at the output. Or using the API. It is an extension of the IPASIR interface with various ways.

For incremental usage, there is also an extension of CDCL, the IPASIR-UP in order to have more fine-grained control.

Proof Format

The solver supports DRAT and LRAT (well tested) and FRAT, but also veriPB (experimental currently)

Official Page

https://github.com/arminbiere/cadical

Other relevant information

The system is under MIT license.

Status

Either: Maintained

References

See the repo for details.