Combining the k-CNF and XOR Phase-Transitions
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 727-733.
Abstract
The runtime performance of modern SAT solvers on random k-CNF formulas is deeply connected with the 'phase-transition' phenomenon seen empirically in the satisfiability of random k-CNF formulas. 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 k-CNF and XOR constraints (known as k-CNF-XOR formulas), but the behavior of random k-CNF-XOR formulas is unexplored in prior work. In this paper, we present the first study of the satisfiability of random k-CNF-XOR formulas. We show empirical evidence of a surprising phase-transition that follows a linear trade-off between k-CNF and XOR constraints. Furthermore, we prove that a phase-transition for k-CNF-XOR formulas exists for k = 2 and (when the number of k-CNF constraints is small) for k > 2.
@inproceedings{ijcai2016p109,
title = {Combining the k-CNF and XOR Phase-Transitions},
author = {Dudek, Jeffrey M. and Meel, Kuldeep S. and Vardi, Moshe Y.},
booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-16}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Subbarao Kambhampati},
pages = {727--733},
year = {2016},
month = {7},
url = {https://ijcai.org/proceedings/2016/109},
}
TY - CPAPER TI - Combining the k-CNF and XOR Phase-Transitions AU - Dudek, Jeffrey M. AU - Meel, Kuldeep S. AU - Vardi, Moshe Y. T2 - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2016 SP - 727 EP - 733 UR - https://ijcai.org/proceedings/2016/109 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
