SATformer: Transformer-Based UNSAT Core Learning
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2022
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909134229602304 |
|---|---|
| author | Shi, Zhengyuan Li, Min Liu, Yi Khan, Sadaf Huang, Junhua Zhen, Hui-Ling Yuan, Mingxuan Xu, Qiang |
| author_facet | Shi, Zhengyuan Li, Min Liu, Yi Khan, Sadaf Huang, Junhua Zhen, Hui-Ling Yuan, Mingxuan Xu, Qiang |
| contents | This paper introduces SATformer, a novel Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. Specifically, it models clause interactions to identify any unsatisfiable sub-problems. Using a graph neural network, we convert clauses into clause embeddings and employ a hierarchical Transformer-based model to understand clause correlation. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core (MUC) for UNSAT problems as clause supervision. As an end-to-end learning-based satisfiability classifier, the performance of SATformer surpasses that of NeuroSAT significantly. Furthermore, we integrate the clause predictions made by SATformer into modern heuristic-based SAT solvers and validate our approach with a logic equivalence checking task. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2209_00953 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | SATformer: Transformer-Based UNSAT Core Learning Shi, Zhengyuan Li, Min Liu, Yi Khan, Sadaf Huang, Junhua Zhen, Hui-Ling Yuan, Mingxuan Xu, Qiang Artificial Intelligence Machine Learning Logic in Computer Science This paper introduces SATformer, a novel Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. Specifically, it models clause interactions to identify any unsatisfiable sub-problems. Using a graph neural network, we convert clauses into clause embeddings and employ a hierarchical Transformer-based model to understand clause correlation. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core (MUC) for UNSAT problems as clause supervision. As an end-to-end learning-based satisfiability classifier, the performance of SATformer surpasses that of NeuroSAT significantly. Furthermore, we integrate the clause predictions made by SATformer into modern heuristic-based SAT solvers and validate our approach with a logic equivalence checking task. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%. |
| title | SATformer: Transformer-Based UNSAT Core Learning |
| topic | Artificial Intelligence Machine Learning Logic in Computer Science |
| url | https://arxiv.org/abs/2209.00953 |