Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2403.03517 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913256179761152 |
|---|---|
| author | Chan, Tsz Ho Xiao, Wenyi Huang, Junhua Zhen, Huiling Tian, Guangji Yuan, Mingxuan |
| author_facet | Chan, Tsz Ho Xiao, Wenyi Huang, Junhua Zhen, Huiling Tian, Guangji Yuan, Mingxuan |
| contents | Boolean Satisfiability problems are vital components in Electronic Design Automation, particularly within the Logic Equivalence Checking process. Currently, SAT solvers are employed for these problems and neural network is tried as assistance to solvers. However, as SAT problems in the LEC context are distinctive due to their predominantly unsatisfiability nature and a substantial proportion of UNSAT-core variables, existing neural network assistance has proven unsuccessful in this specialized domain. To tackle this challenge, we propose IB-Net, an innovative framework utilizing graph neural networks and novel graph encoding techniques to model unsatisfiable problems and interact with state-of-the-art solvers. Extensive evaluations across solvers and datasets demonstrate IB-Net's acceleration, achieving an average runtime speedup of 5.0% on industrial data and 8.3% on SAT competition data empirically. This breakthrough advances efficient solving in LEC workflows. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_03517 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | IB-Net: Initial Branch Network for Variable Decision in Boolean Satisfiability Chan, Tsz Ho Xiao, Wenyi Huang, Junhua Zhen, Huiling Tian, Guangji Yuan, Mingxuan Artificial Intelligence Boolean Satisfiability problems are vital components in Electronic Design Automation, particularly within the Logic Equivalence Checking process. Currently, SAT solvers are employed for these problems and neural network is tried as assistance to solvers. However, as SAT problems in the LEC context are distinctive due to their predominantly unsatisfiability nature and a substantial proportion of UNSAT-core variables, existing neural network assistance has proven unsuccessful in this specialized domain. To tackle this challenge, we propose IB-Net, an innovative framework utilizing graph neural networks and novel graph encoding techniques to model unsatisfiable problems and interact with state-of-the-art solvers. Extensive evaluations across solvers and datasets demonstrate IB-Net's acceleration, achieving an average runtime speedup of 5.0% on industrial data and 8.3% on SAT competition data empirically. This breakthrough advances efficient solving in LEC workflows. |
| title | IB-Net: Initial Branch Network for Variable Decision in Boolean Satisfiability |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2403.03517 |