---
title: "Combining the k-CNF and XOR Phase-Transitions"
authors:
  - "Jeffrey M. Dudek"
  - "Kuldeep S. Meel"
  - "Moshe Y. Vardi"
doi: ""
url: "https://ijcai.org/proceedings/2016/109"
pdf: "https://ijcai.org/proceedings/2016/0109.pdf"
venue: "Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence"
year: 2016
pages: "727-733"
track: ""
keywords:
---

# Combining the k-CNF and XOR Phase-Transitions

Jeffrey M. Dudek, Kuldeep S. Meel, Moshe Y. Vardi

*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.