Skip to content

alan23273850/cadical

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

License: MIT Build Status

CaDiCaL Simplified Satisfiability Solver

The original goal of the development of CaDiCaL was to obtain a CDCL solver, which is easy to understand and change, while at the same time not being much slower than other state-of-the-art CDCL solvers. Originally we wanted to also radically simplify the design and internal data structures, but that goal was only achieved partially, at least for instance compared to Lingeling.

However, the code is much better documented and on the other hand CaDiCaL actually became in general faster than Lingeling even though it is missing some preprocessors (mostly parity and cardinality constraint reasoning), which would be crucial to solve certain instances.

Use ./configure && make to configure and build cadical and the library libcadical.a in the default build sub-directory. The header file of the library is src/cadical.hpp and includes an example for API usage.

See BUILD.md for options and more details related to the build process and test/README.md for testing the library and the solver.

The solver has the following usage cadical [ dimacs [ proof ] ]. See cadical -h for more options.

The latest version can be found at http://fmv.jku.at/cadical.

Armin Biere

About

CaDiCaL SAT Solver

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • C++ 89.8%
  • C 7.2%
  • Shell 2.9%
  • Makefile 0.1%