Presentation
X-SAT: An Efficient Circuit-Based SAT Solver
DescriptionIn modern digital circuit design, verifying the equivalence of arithmetic circuits is a significant and challenging task. This paper introduces a new circuit solver based on the Conflict-Driven Clause Learning (CDCL) algorithm, which integrates structural elimination techniques to reduce the number of variables and clauses while maintaining the circuit structure. Additionally, branching heuristics have been enhanced specifically for the structure of arithmetic circuits. Experimental results demonstrate that X-SAT significantly outperforms best previous circuit solver could be found on all benchmarks. Further, X-SAT performs better than the state-of-the-art CNF-based SAT solvers on complex arithmetic circuits, underscoring its significant potential in the field of circuit design verification.
Event Type
Research Manuscript
TimeWednesday, June 253:45pm - 4:00pm PDT
Location3004, Level 3
EDA
EDA2: Design Verification and Validation
Similar Presentations