GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929348074799104 |
|---|---|
| author | Zhang, Zhanguang Chetelat, Didier Cotnareanu, Joseph Ghose, Amur Xiao, Wenyi Zhen, Hui-Ling Zhang, Yingxue Hao, Jianye Coates, Mark Yuan, Mingxuan |
| author_facet | Zhang, Zhanguang Chetelat, Didier Cotnareanu, Joseph Ghose, Amur Xiao, Wenyi Zhen, Hui-Ling Zhang, Yingxue Hao, Jianye Coates, Mark Yuan, Mingxuan |
| contents | Boolean satisfiability (SAT) problems are routinely solved by SAT solvers in real-life applications, yet solving time can vary drastically between solvers for the same instance. This has motivated research into machine learning models that can predict, for a given SAT instance, which solver to select among several options. Existing SAT solver selection methods all rely on some hand-picked instance features, which are costly to compute and ignore the structural information in SAT graphs. In this paper we present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances and a heterogeneous graph neural network (GNN) model. While GNNs have been previously adopted in other SAT-related tasks, they do not incorporate any domain-specific knowledge and ignore the runtime variation introduced by different clause orders. We enrich the graph representation with domain-specific decisions, such as novel node feature design, positional encodings for clauses in the graph, a GNN architecture tailored to our tripartite graphs and a runtime-sensitive loss function. Through extensive experiments, we demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime for a pool of seven state-of-the-art solvers on both an industrial circuit design benchmark, and on instances from the 20-year Anniversary Track of the 2022 SAT Competition. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_11024 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection Zhang, Zhanguang Chetelat, Didier Cotnareanu, Joseph Ghose, Amur Xiao, Wenyi Zhen, Hui-Ling Zhang, Yingxue Hao, Jianye Coates, Mark Yuan, Mingxuan Machine Learning Artificial Intelligence Boolean satisfiability (SAT) problems are routinely solved by SAT solvers in real-life applications, yet solving time can vary drastically between solvers for the same instance. This has motivated research into machine learning models that can predict, for a given SAT instance, which solver to select among several options. Existing SAT solver selection methods all rely on some hand-picked instance features, which are costly to compute and ignore the structural information in SAT graphs. In this paper we present GraSS, a novel approach for automatic SAT solver selection based on tripartite graph representations of instances and a heterogeneous graph neural network (GNN) model. While GNNs have been previously adopted in other SAT-related tasks, they do not incorporate any domain-specific knowledge and ignore the runtime variation introduced by different clause orders. We enrich the graph representation with domain-specific decisions, such as novel node feature design, positional encodings for clauses in the graph, a GNN architecture tailored to our tripartite graphs and a runtime-sensitive loss function. Through extensive experiments, we demonstrate that this combination of raw representations and domain-specific choices leads to improvements in runtime for a pool of seven state-of-the-art solvers on both an industrial circuit design benchmark, and on instances from the 20-year Anniversary Track of the 2022 SAT Competition. |
| title | GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection |
| topic | Machine Learning Artificial Intelligence |
| url | https://arxiv.org/abs/2405.11024 |