{
"id": "1702.08392",
"version": "v1",
"published": "2017-02-27T17:38:31.000Z",
"updated": "2017-02-27T17:38:31.000Z",
"title": "Combining the $k$-CNF and XOR Phase-Transitions",
"authors": [
"Jeffrey M. Dudek",
"Kuldeep S. Meel",
"Moshe Y. Vardi"
],
"comment": "Presented at The 25th International Joint Conference on Artificial Intelligence (IJCAI-16)",
"categories": [
"cs.DM"
],
"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$.",
"revisions": [
{
"version": "v1",
"updated": "2017-02-27T17:38:31.000Z"
}
],
"analyses": {
"keywords": [
"cnf-xor formulas",
"xor phase-transitions",
"cnf formulas",
"runtime performance",
"xor constraints"
],
"tags": [
"conference paper"
],
"note": {
"typesetting": "TeX",
"pages": 0,
"language": "en",
"license": "arXiv",
"status": "editable"
}
}
}