Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913922309685248 |
|---|---|
| author | Shi, Zhengyuan Tang, Tiebing Zhu, Jiaying Khan, Sadaf Zhen, Hui-Ling Yuan, Mingxuan Chu, Zhufei Xu, Qiang |
| author_facet | Shi, Zhengyuan Tang, Tiebing Zhu, Jiaying Khan, Sadaf Zhen, Hui-Ling Yuan, Mingxuan Chu, Zhufei Xu, Qiang |
| contents | The Circuit Satisfiability (CSAT) problem, a variant of the Boolean Satisfiability (SAT) problem, plays a critical role in integrated circuit design and verification. However, existing SAT solvers, optimized for Conjunctive Normal Form (CNF), often struggle with the intrinsic complexity of circuit structures when directly applied to CSAT instances. To address this challenge, we propose a novel preprocessing framework that leverages advanced logic synthesis techniques and a reinforcement learning (RL) agent to optimize CSAT problem instances. The framework introduces a cost-customized Look-Up Table (LUT) mapping strategy that prioritizes solving efficiency, effectively transforming circuits into simplified forms tailored for SAT solvers. Our method achieves significant runtime reductions across diverse industrial-scale CSAT benchmarks, seamlessly integrating with state-of-the-art SAT solvers. Extensive experimental evaluations demonstrate up to 63\% reduction in solving time compared to conventional approaches, highlighting the potential of EDA-driven innovations to advance SAT-solving capabilities. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_19446 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving Shi, Zhengyuan Tang, Tiebing Zhu, Jiaying Khan, Sadaf Zhen, Hui-Ling Yuan, Mingxuan Chu, Zhufei Xu, Qiang Logic in Computer Science The Circuit Satisfiability (CSAT) problem, a variant of the Boolean Satisfiability (SAT) problem, plays a critical role in integrated circuit design and verification. However, existing SAT solvers, optimized for Conjunctive Normal Form (CNF), often struggle with the intrinsic complexity of circuit structures when directly applied to CSAT instances. To address this challenge, we propose a novel preprocessing framework that leverages advanced logic synthesis techniques and a reinforcement learning (RL) agent to optimize CSAT problem instances. The framework introduces a cost-customized Look-Up Table (LUT) mapping strategy that prioritizes solving efficiency, effectively transforming circuits into simplified forms tailored for SAT solvers. Our method achieves significant runtime reductions across diverse industrial-scale CSAT benchmarks, seamlessly integrating with state-of-the-art SAT solvers. Extensive experimental evaluations demonstrate up to 63\% reduction in solving time compared to conventional approaches, highlighting the potential of EDA-driven innovations to advance SAT-solving capabilities. |
| title | Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2403.19446 |