Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912406326738944 |
|---|---|
| author | Zhang, Zhiwei Fung, Samy Wu Kyrillidis, Anastasios Osher, Stanley Vardi, Moshe Y. |
| author_facet | Zhang, Zhiwei Fung, Samy Wu Kyrillidis, Anastasios Osher, Stanley Vardi, Moshe Y. |
| contents | The Boolean satisfiability (SAT) problem lies at the core of many applications in combinatorial optimization, software verification, cryptography, and machine learning. While state-of-the-art solvers have demonstrated high efficiency in handling conjunctive normal form (CNF) formulas, numerous applications require non-CNF (hybrid) constraints, such as XOR, cardinality, and Not-All-Equal constraints. Recent work leverages polynomial representations to represent such hybrid constraints, but it relies on box constraints that can limit the use of powerful unconstrained optimizers. In this paper, we propose unconstrained continuous optimization formulations for hybrid SAT solving by penalty terms. We provide theoretical insights into when these penalty terms are necessary and demonstrate empirically that unconstrained optimizers (e.g., Adam) can enhance SAT solving on hybrid benchmarks. Our results highlight the potential of combining continuous optimization and machine-learning-based methods for effective hybrid SAT solving. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_00674 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization Zhang, Zhiwei Fung, Samy Wu Kyrillidis, Anastasios Osher, Stanley Vardi, Moshe Y. Logic in Computer Science Artificial Intelligence Machine Learning Optimization and Control The Boolean satisfiability (SAT) problem lies at the core of many applications in combinatorial optimization, software verification, cryptography, and machine learning. While state-of-the-art solvers have demonstrated high efficiency in handling conjunctive normal form (CNF) formulas, numerous applications require non-CNF (hybrid) constraints, such as XOR, cardinality, and Not-All-Equal constraints. Recent work leverages polynomial representations to represent such hybrid constraints, but it relies on box constraints that can limit the use of powerful unconstrained optimizers. In this paper, we propose unconstrained continuous optimization formulations for hybrid SAT solving by penalty terms. We provide theoretical insights into when these penalty terms are necessary and demonstrate empirically that unconstrained optimizers (e.g., Adam) can enhance SAT solving on hybrid benchmarks. Our results highlight the potential of combining continuous optimization and machine-learning-based methods for effective hybrid SAT solving. |
| title | Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization |
| topic | Logic in Computer Science Artificial Intelligence Machine Learning Optimization and Control |
| url | https://arxiv.org/abs/2506.00674 |