CDCLsat

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.

1. Download and install the Julia language.
2. Start the Julia REPL.
3. 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 variable
• vsids_increment::Int – increment of the VSIDS conflict counter for variables involved in a conflict
• vsids_increase::Int – increase of the VSIDS increment after each conflict
• vsids_period::Int – number of conflicts per VSIDS period
• vsids_decay::Float64 – multiplier for both VSIDS increment and conflict counters at the end of a period
• output::BoolOrNothing – output events and assignments (true), only model and solution (false), or nothing

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)

• DataStructures.jl
• Formatting.jl
• RomanNumerals.jl
• Term.jl

• 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