• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas.
Jeffrey Dudek, Kuldeep S. Meel and Moshe Y. Vardi.
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), August 2017.
Recent universal-hashing based approaches to sampling and counting crucially depend on the runtime performance of \SAT solvers on formulas expressed as the conjunction of both CNF constraints and variable-width XOR constraintsints (known as CNF-XOR formulas). In this paper, we present the first study of the runtime behavior of \SAT solvers equipped with XOR-reasoning techniques on random CNF-XOR formulas. We empirically demonstrate that a state-of-the-art \SAT solver scales exponentially on random CNF-XOR formulas across a wide range of XOR-clause densities, peaking around the empirical phase-transition location. On the theoretical front, we prove that the solution space of a random CNF-XOR formula `shatters' at all nonzero XOR-clause densities into well-separated components, similar to the behavior seen in random CNF formulas known to be difficult for many \SAT-solving algorithms.
@inproceedings{DMV17,
title={The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas},
author={Dudek, Jeffrey and Meel, Kuldeep S. and Vardi, Moshe Y.},
year={2017},
booktitle=IJCAI,
month=aug,
bib2html_dl_pdf={../Papers/ijcai17.pdf},
bib2html_pubtype={Refereed Conference},
bib2html_rescat={Phase Transitions},
abstract={Recent universal-hashing based approaches to sampling and counting
crucially depend on the runtime performance of \SAT~solvers on
formulas expressed as the conjunction of both CNF constraints and variable-width XOR constraintsints (known as CNF-XOR formulas). In this paper, we present the first study of the runtime behavior of \SAT~solvers equipped with XOR-reasoning techniques on random CNF-XOR formulas.
We empirically demonstrate that a state-of-the-art \SAT~solver scales exponentially on random CNF-XOR formulas across a wide range of XOR-clause densities, peaking around the empirical phase-transition location.
On the theoretical front, we prove that the solution space of a
random CNF-XOR formula `shatters' at \emph{all} nonzero XOR-clause densities
into well-separated components, similar to the behavior seen in random CNF formulas
known to be difficult for many \SAT-solving algorithms.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Sun Apr 14, 2024 11:15:51