Using deep learning to construct stochastic local search SAT solvers with performance bounds
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910133394604032 |
|---|---|
| author | Kramer, Maximilian J. Boes, Paul Eisert, Jens |
| author_facet | Kramer, Maximilian J. Boes, Paul Eisert, Jens |
| contents | The Boolean Satisfiability problem (SAT), as the prototypical $\mathsf{NP}$-complete problem, is crucial in both theoretical computer science and practical applications. To address this problem, stochastic local search (SLS) algorithms, which iteratively and randomly update candidate assignments, present an important and theoretically well-studied class of solvers. Recent theoretical advancements have identified conditions under which SLS solvers efficiently solve SAT instances, provided they have access to suitable ``oracles'', i.e., instance-specific distribution samples. We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers. Our approach, evaluated on random and pseudo-industrial SAT instances, demonstrates a significant performance improvement regarding step counts and solved instances. Our work bridges theoretical results and practical applications, highlighting the potential of purpose-trained SAT solvers with performance guarantees. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2309_11452 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Using deep learning to construct stochastic local search SAT solvers with performance bounds Kramer, Maximilian J. Boes, Paul Eisert, Jens Artificial Intelligence Optimization and Control The Boolean Satisfiability problem (SAT), as the prototypical $\mathsf{NP}$-complete problem, is crucial in both theoretical computer science and practical applications. To address this problem, stochastic local search (SLS) algorithms, which iteratively and randomly update candidate assignments, present an important and theoretically well-studied class of solvers. Recent theoretical advancements have identified conditions under which SLS solvers efficiently solve SAT instances, provided they have access to suitable ``oracles'', i.e., instance-specific distribution samples. We propose leveraging machine learning models, particularly graph neural networks (GNN), as oracles to enhance the performance of SLS solvers. Our approach, evaluated on random and pseudo-industrial SAT instances, demonstrates a significant performance improvement regarding step counts and solved instances. Our work bridges theoretical results and practical applications, highlighting the potential of purpose-trained SAT solvers with performance guarantees. |
| title | Using deep learning to construct stochastic local search SAT solvers with performance bounds |
| topic | Artificial Intelligence Optimization and Control |
| url | https://arxiv.org/abs/2309.11452 |