Lean SAT Reference Implementation

Prompt file imported from jetafese/leanSat (.github/prompts/lean-sat-reference.prompt.md). Copyright stays with the author.

Create a reference implementation of a Boolean satisfiability (SAT) solver in Lean.

Default profile (use unless prompt arguments override):

• Baseline: DPLL with unit propagation and backtracking; include explicit extension hooks for a future CDCL layer.
• Input: support both direct Lean CNF AST construction and a simple DIMACS CNF parser.
• Proof target: establish soundness and completeness for the baseline solver; include termination reasoning for core recursive search.
• Layering: separate Core (executable algorithm/data) and Verified (semantics/proofs) modules.
• Heuristics: start with a simple branching heuristic (first-unassigned or similar), pluggable behind an interface.
• Validation: provide theorem-style examples plus lightweight property-style checks where practical.
• Delivery style: generate incrementally file-by-file with short checkpoints, while still producing runnable integrated code.

Primary goal:

• Build a clean, modular architecture that can be extended with optimizations and later evolved into an efficient SMT solver.

Required outcomes:

• Implement core SAT data structures (literals, clauses, CNF formulas, assignments, solver state).
• Implement parsing or constructors for CNF test inputs (keep this simple but structured for extension).
• Implement a baseline complete SAT procedure (for example: DPLL-style search with unit propagation and backtracking).
• Separate interfaces from implementations so improved heuristics can be added without rewriting core logic.
• Include correctness-oriented Lean definitions and proofs for key properties of the baseline solver.

Design constraints:

• Keep modules small and focused, with clear boundaries.
• Favor explicit types and invariants over implicit assumptions.
• Avoid tightly coupling heuristics to the core search engine.
• Document extension points for future features such as watched literals, clause learning, and theory propagation.

Verification expectations:

• Prove core semantic links, such as:
  • Assignment satisfaction relation for literals, clauses, and CNF formulas.
  • Soundness of propagation/search steps (reported SAT implies a satisfying assignment).
  • Basic termination argument or structurally recursive organization for the baseline solver.
• If full completeness proof is too large, provide a staged proof plan and prove the most critical lemmas needed for eventual completeness.

Implementation quality:

• Use readable Lean code with brief comments where logic is subtle.
• Include a file/module layout proposal before coding, then implement it.
• Add small executable examples or tests that demonstrate SAT and UNSAT cases.
• Explain tradeoffs in design decisions that affect future SMT integration.

Output format:

1. Short architecture plan.
2. Module-by-module Lean code.
3. Proof sketch and completed proofs.
4. Example runs/tests.
5. Next optimization roadmap toward an SMT-capable core.

If the user provides additional requirements in the prompt argument, incorporate them while preserving modularity and proof-driven design.

When requirements conflict, prioritize: correctness and proof clarity, then modularity/extension design, then raw performance.