• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Combining the k-CNF and XOR Phase-Transitions.
Jeffrey Dudek, Kuldeep S. Meel and Moshe Y. Vardi.
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), July 2016.
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{DMV16,
title={Combining the k-CNF and XOR Phase-Transitions},
author={Dudek, Jeffrey and Meel, Kuldeep S. and Vardi, Moshe Y.},
bib2html_dl_pdf={../Papers/ijcai16-cnfxor.pdf},
code={http://www.cs.rice.edu/CS/Verification/Projects/CUSP/IJCAI16/},
year={2016},
month=jul,
booktitle=IJCAI,
bib2html_rescat={Phase Transitions},
bib2html_pubtype={Refereed Conference},
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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Tue Apr 28, 2026 01:27:21