Home

Basic CDCL Interactive Lab

Conflict-Driven Clause Learning — step-by-step exploration

Formula Input (CNF)
Syntax: | or ∨ between literals in clause  ·  , or & between clauses  ·  - or ¬ for negation
Examples:
CDCL Actions
What can I do?
Load a formula to begin.
Conflict Clause K (being analyzed)
Formula (F)  
Load a formula to see clauses.
Variable Assignments
—
Assignment Trail (M) by Decision Level
Decision Propagated
M = ∅
Rule Explanation

Apply an action to see a detailed explanation of the CDCL rule used.

Step History
Choose a Literal to Decide
Pick an unassigned variable. This is a free choice — it will be added to both M (trail) and D (decision set), marking a backjump point.
— or pick manually —
Choose a Unit to Propagate
Choose Backjump Target
Choose a Conflict Clause
Choose a Resolution Step
Decision Heuristics
Each heuristic analyzes the current formula to suggest which literal to decide. Click Decide → to use the suggestion, or go back to pick manually.

  






  
Lab Files


  

    

      🐍 Source Code ▼
    

    

      
        basic-cdcl-solver.py
        PY
        View
      
      
        basic-cdcl-solver-debug.py
        PY
        View