abhamra/verified-CDCL-datastructures
1
0
Fork 0
mirror of https://github.com/abhamra/verified-CDCL-datastructures synced 2026-11-12 00:41:03 -08:00
Code Issues Projects Releases Packages Wiki Activity
No description
65 commits 4 branches 0 tags 1,020 KiB
  • Lean 100%
Find a file
Exact
Arjun Bhamra 59fc043ae5 added final project zip
2025-12-05 23:37:18 -05:00
images finished slides, except for the bcp proofs part 2025-12-01 19:13:37 -05:00
VerifiedCdclDatastructures quickfix bcp 2025-12-05 22:42:00 -05:00
.gitignore initializing lean project 2025-09-30 14:34:07 -04:00
8803_final_proj.zip added final project zip 2025-12-05 23:37:18 -05:00
Final Report.pdf added final project zip 2025-12-05 23:37:18 -05:00
lake-manifest.json pushing so I don't lose anything, first pass VSIDS not much progress 2025-10-25 17:30:32 -04:00
lakefile.lean pushing so I don't lose anything, first pass VSIDS not much progress 2025-10-25 17:30:32 -04:00
lean-toolchain pushing so I don't lose anything, first pass VSIDS not much progress 2025-10-25 17:30:32 -04:00
LICENSE Initial commit 2025-09-30 14:32:57 -04:00
proj_pres.md proj pres pdf uploaded 2025-12-05 23:33:16 -05:00
proj_pres.pdf proj pres pdf uploaded 2025-12-05 23:33:16 -05:00
README.md Create README.md 2025-09-30 14:54:30 -04:00
VerifiedCdclDatastructures.lean first pass for data structures, code organization 2025-10-03 17:08:27 -04:00

README.md

Verified CDCL Data Structures

Arjun Bhamra and Cameron Hoechst

As a part of our 8803 Special Topics course on SAT/SMT Solvers, we are aiming to create a verified set of data structures for use in the CDCL SAT Solver algorithm. The data structures we intend to focus on are:

  1. Conflict/Implication Graph
  2. (Conflict) Clauses
  3. Partial (Learned) Clause Database
  4. Assignment Trail

Later on, we may begin leveraging these data structures to implement CDCL properly.