Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method
Abstract
A recent success of SAT solving has been the solution of the boolean Pythagorean Triples problem [Heule et al., 2016], delivering the largest proof yet, of 200 terabytes in size. We present this and the underlying paradigm Cube-and-Conquer, a powerful general method to solve big SAT problems, based on integrating the “old” and “new” methods of SAT solving.
Cite
Text
Heule et al. "Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method." International Joint Conference on Artificial Intelligence, 2017. doi:10.24963/IJCAI.2017/683Markdown
[Heule et al. "Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method." International Joint Conference on Artificial Intelligence, 2017.](https://mlanthology.org/ijcai/2017/heule2017ijcai-solving/) doi:10.24963/IJCAI.2017/683BibTeX
@inproceedings{heule2017ijcai-solving,
title = {{Solving Very Hard Problems: Cube-and-Conquer, a Hybrid SAT Solving Method}},
author = {Heule, Marijn J. H. and Kullmann, Oliver and Marek, Victor W.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2017},
pages = {4864-4868},
doi = {10.24963/IJCAI.2017/683},
url = {https://mlanthology.org/ijcai/2017/heule2017ijcai-solving/}
}