Expand description
The cdcl module implements the Conflict-Driven Clause Learning (CDCL) algorithm for SAT solving.
Implements the core Conflict-Driven Clause Learning (CDCL) SAT solver.
The Cdcl struct orchestrates various components like variable selection,
propagation, conflict analysis, and clause learning to determine the
satisfiability of a given Conjunctive Normal Form (CNF) formula.
It follows the typical CDCL algorithm structure, including decision-making,
boolean constraint propagation (BCP), conflict analysis, clause learning,
non-chronological backtracking, and restarts.
Structsยง
- Cdcl
- Represents a CDCL SAT solver instance.