CDCL SAT Solver
Check satisfiability (SAT) of a propositional logic formula in Conjunctive Normal Form (CNF) using the Davis-Putnam-Logemann-Loveland (DPLL) algorithm with Boolean Constraint Propagation (BCP), Conflict-Driven Clause Learning (CDCL), and the Variable State Independent Decaying Sum (VSIDS) decision heuristics.
- Download and install the Julia language.
- Start the Julia REPL.
- Type the following to enter the Pkg REPL and install the package:
julia> ]
pkg> add CDCLsat
Create a model using the constructor Model().
The following model parameters / fields may be set:
decision::Bool– assignment used when making a heuristics-based decision for a variablevsids_increment::Int– increment of the VSIDS conflict counter for variables involved in a conflictvsids_increase::Int– increase of the VSIDS increment after each conflictvsids_period::Int– number of conflicts per VSIDS periodvsids_decay::Float64– multiplier for both VSIDS increment and conflict counters at the end of a periodoutput::BoolOrNothing– output events and assignments (true), only model and solution (false), ornothing
Add variables using the macro @variable <model> <name> (<priority>|ε).
Add clauses using the macro @clause <model> <name> [ (¬|!|ε)<variable> ... ].
Solve the model with the function solve!(model::Model).
If the formula is satisfiable, a satisfying assignment can be obtained from the model field variables by accessing the field assignment of each Variable.
Note that a model should not be reused.
using CDCLsat
model = Model()
@variable model x
@variable model y
@clause model c1 [x y]
@clause model c2 [!x !y]
@clause model c3 [!x y]
@clause model c4 [x !y]
solve!(model)- Erika Ábrahám: RWTH Satisfiability Checking Lecture
- João P. Marques-Silva, Karem A. Sakallah: GRASP – A New Search Algorithm for Satisfiability, GRASP: A Search Algorithm for Propositional Satisfiability
- Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik: Chaff: Engineering an Efficient SAT Solver