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:
- Conflict/Implication Graph
- (Conflict) Clauses
- Partial (Learned) Clause Database
- Assignment Trail
Later on, we may begin leveraging these data structures to implement CDCL properly.