Combining the $k$-CNF and XOR Phase-Transitions
Jeffrey M. Dudek Kuldeep S. Meel Moshe Y. Vardi


Definition of the relativistic geoid in terms of isochronometric surfaces
    Dennis Philipp, Volker Perlick, Dirk Puetzfeld, Eva Hackmann, and Claus Lämmerzahl
    
======================================================================================








	/cnfxor/.is family, /cnfxor,
	default/.style = k = k, n = n, r = r, s = s, cnfNum = , xorNum = ,
	k/.estore in = ,
	n/.estore in = ,
	r/.estore in = ,
	s/.estore in = ,
	cnfNum/.estore in = ,
	xorNum/.estore in = ,

























theoremTheorem
lemma[theorem]Lemma
corollary[theorem]Corollary

conjectureConjecture
speculationSpeculation



The runtime performance of modern  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  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.




§ INTRODUCTION


The Constraint-Satisfaction Problem (CSP) is one of the most fundamental problem in 
computer science, with a wide range of applications arising from diverse areas 
such as artificial intelligence, programming languages, biology and the like <cit.>.
The problem is, in general, NP-complete, and the study of run-time behavior of CSP
techniques is a topic of major interest in AI, cf. <cit.>. Of specific interest
is the behavior of CSP solvers on random problems <cit.>. Specifically, a deep
connection was discovered between the density (ratio of clauses to variables) of random
propositional CNF fixed-width (fixed number of literals per clause) formulas and the runtime 
behavior of SAT solvers on such formulas <cit.>. The key experimental findings
are: (1) as the density of random CNF instances increases, the probability of satisfiability 
decreases with a precipitous drop, believed to be a phase-transition, around the point 
where the satisfiability probability is 0.5, and (2) instances at the phase-transition point 
are particularly challenging for DPLL-based SAT solvers.  Indeed, phase-transition instances 
serve as a source of challenging benchmark problems in  competitions <cit.>. 
The connection between runtime performance and the satisfiability phase-transition has propelled 
the study of such phase-transition phenomena over the past two decades <cit.>, 
including detailed studies of how SAT solvers scale at different densities <cit.>.

For random k-CNF formulas, where every clause contains exactly k literals, experiments
suggest a specific phase-transition density, for example, density 4.26 for random 3-SAT,
but establishing this analytically has been highly challenging <cit.>, and it has been
established only for for k=2 <cit.> and all large enough k <cit.>. 
A phase-transition phenomenon has also been identified in random XOR formulas (conjunctions of 
XOR constraints). 
Creignou and Daudé CD99 proved a phase-transition at density 1 for variable-width 
random XOR formulas.  Creignou and Daudé CD03 also proved the existence of a phase 
transition for random ℓ-XOR formulas (where each XOR-clause contains exactly ℓ literals), for ℓ≥ 1,  
without specifying an exact location for the phase-transition. Dubois and Mandler DM02 independently identified the location of a phase transition for random 3-XOR formulas. More recently, Pittel and 
Sorkin PS15 identified the location of the phase-transition for ℓ-XOR formulas for ℓ > 3.

Despite the abundance of prior work on the phase-transition phenomenon in the satisfiability of 
random k-CNF formulas and XOR formulas, no prior work considers the satisfiability of 
random formulas with both k-clauses and variable-width XOR-clauses together, 
henceforth referred as k-CNF-XOR formulas. Recently, successful hashing-based 
approaches to the fundamental problems of constrained sampling and counting employ  
solvers to solve k-CNF-XOR formulas <cit.>. Unlike previous approaches 
to sampling and counting, hashing-based approaches provide strong theoretical guarantees and 
scale to real-world instances involving formulas with hundreds of thousands of variables. 
The scalability of these approaches crucially depends on the runtime performance of 
 solvers in handling k-CNF-XOR formulas  <cit.>. Moreover, since the phase-transition behavior of k-CNF constraints have been analyzed to explain runtime behavior of  solvers <cit.>, we believe that analysis of the phase-transition phenomenon for k-CNF-XOR formula is the first step towards demystifying the runtime behavior of CNF-XOR solvers such as CryptoMiniSAT <cit.> and thus explain the runtime behavior of hashing-based algorithms.


The primary contribution of this work is the first study of phase-transition phenomenon in the satisfiability of random k-CNF-XOR formulas, henceforth referred to as the k-CNF-XOR phase-transition. In particular:

	
  * We present (in Section <ref>) experimental evidence for a k-CNF-XOR phase-transition that follows a linear trade-off between k-CNF clauses and XOR clauses.
	
  * We prove (in Section <ref>) that the k-CNF-XOR phase-transition exists when the ratio of k-CNF clauses to variables is small. This fully characterizes the phase-transition when k=2.
	
  * We prove (in Section <ref>) upper and lower bounds on the location of the k-CNF-XOR  phase-transition region.
	
  * We conjecture (in Section <ref>) that the exact location of a phase-transition for k ≥ 3 follows the linear trade-off between k-CNF and XOR clauses seen experimentally.




§ NOTATIONS AND PRELIMINARIES
 
Let X = {X_1, ⋯, X_n} be a set of propositional variables and 
let F be a formula defined over X. A satisfying assignment or 
witness of F is an assignment of truth values to the variables in X such that F evaluates to true. Let #F denote the number of satisfying 
assignments of F. We say that F is satisfiable (or sat.) if #F > 0 and 
that F is unsatisfiable (or unsat.) if #F = 0.

We use (X) to denote the probability of event X. 
We say that an infinite sequence of random events E_1, E_2, ⋯ occurs 
with high probability (denoted, w.h.p.) if lim_n →∞(E_n) = 1. We use Y and Y to denote respectively the expected value and variance of a random variable Y. We use YZ to denote the covariance of random variables Y and Z. We use o_k(1) to denote a term which converges to 0 as k →∞.

A k-clause is the disjunction of k literals out of { X_1, ⋯, X_n}, 
with each variable possibly negated. For fixed positive integers k and n and 
a nonnegative real number r, let the random variable  
denote the formula consisting of the conjunction of rn k-clauses, with each clause chosen 
uniformly and independently from all nk2^k possible k-clauses over n variables.

The early experiments on  <cit.> led to the following conjecture:

	For every integer k ≥ 2, there is a critical ratio r_k such that:
	
		
  * If r < r_k, then  is satisfiable w.h.p.
		
  * If r > r_k, then  is unsatisfiable w.h.p.
	

The Conjecture was quickly proved for k=2, where r_2 = 1 <cit.>. 
In recent work, Ding, Sly, and Sun established the Satisfiability Phase Transition Conjecture 
for all sufficiently large k <cit.>. The Conjecture has remained elusive for small values 
of k ≥ 3, although values for these critical ratios r_k can be estimated experimentally, 
e.g., r_3 seems to be near 4.26.

An XOR-clause over n variables is the `exclusive or' of either 0 or 1 together with a subset 
of the variables X_1, ⋯, X_n. An XOR-clause including 0 (respectively, 1) evaluates to true if and only 
if an odd (respectively, even) number of the included variables evaluate to true. 
Note that all k-clauses contain exactly k variables, whereas the number of variables 
in an XOR-clause is not fixed; a uniformly chosen XOR-clause over n variables contains 
n/2 variables in expectation. 

For a fixed positive integer n and a nonnegative 
real number s, let the random variable  denote 
the formula consisting of the conjunction of sn XOR-clauses, with each clause chosen uniformly 
and independently from all 2^n+1 XOR-clauses over n variables. 
Creignou and Daude CD99,CD03 proved a phase-transition in the satisfiability of : if s < 1 then  is satisfiable w.h.p., 
while if s > 1 then  is unsatisfiable w.h.p. 

A k-CNF-XOR formula is the conjunction of some number of k-clauses and XOR-clauses. 
For fixed positive integers k and n and fixed nonnegative real numbers r and 
s, let the random variable  denote the 
formula consisting of the conjunction of rn k-clauses and sn XOR-clauses, 
with each clause chosen uniformly and independently from all possible k-clauses and 
XOR-clauses over n variables. (The motivation for using
fixed-width clauses and variable-width XOR-clauses comes from the hashing-based approaches to
constrained sampling and counting discussed in Section <ref>.) Although random k-CNF formulas and XOR formulas have been well studied separately, 
no prior work considers the satisfiability of random mixed formulas arising 
from conjunctions of k-clauses and XOR-clauses. 



§ EXPERIMENTAL RESULTS
 
To explore empirically the behavior of the satisfiability of k-CNF-XOR 
formulas, we built a prototype implementation in Python that employs the 
[<http://www.msoos.org/cryptominisat4/>] <cit.> 
solver to check satisfiability of k-CNF-XOR formulas. We chose  
due to its ability to handle the combination of k-clauses and XOR-clauses efficiently <cit.>. 
The objective of the experimental setup was to empirically determine the behavior of 
( is sat) with respect to r and s, the k-clause and XOR-clause 
densities respectively, for fixed k and n. 



 §.§ Experimental Setup

We ran 11 experiments with various values of k and n. For k=2, we ran experiments for n ∈{25,50,100,150}. For k=3, we ran experiments for n ∈{25, 50, 100}. For k = 4 and k=5, we ran experiments for n ∈{25, 50}. We were not able to run experiments for values of n significantly larger than those listed above: at some k-clause and XOR-clause densities, the run-time of  scaled far beyond our computational capabilities.

In each experiment, the XOR-clause 
density s ranged from 0 to 1.2 in increments of 0.02. Since the location of phase-transition 
for k-CNF depends on k, the range of k-clause density r also depends 
on k. For k=3, r ranged from from 0 to 6 in increments of 0.04;
for k=5, r ranged from 0 to 26 in increments of 0.43, and the like.

To uniformly choose a k-clause we uniformly selected without replacement 
k out of the variables {X_1, ⋯, X_n}. For each selected variable X_i, 
we include exactly one of the literals X_i or X_i in the k-clause, 
each with probability 1/2. The disjunction of these k literals is 
a uniformly chosen k-clause.  To uniformly choose an XOR-clause, we include 
each variable of {X_1, ⋯, X_n} with probability 1/2 in a set 
A of variables. Additionally we include in A exactly one of 0 or 1, 
each with probability 1/2. The `exclusive-or' of all elements of A 
is a uniformly chosen XOR-clause.

For each assignment of values to k, n, r, and s, we evaluated satisfiability, 
using , of 100 uniformly generated formulas of  by constructing 
the conjunction of rn k-clauses and sn XOR-clauses, with each clause chosen uniformly 
and independently as described above. The percentage of satisfiable formulas gives us an empirical estimate of ( is satisfiable).

Each experiment was run on a node within a high-performance computer cluster. 
These nodes contain 12-processor cores at 2.83 GHz each with 48 GB of RAM per node. 
Each formula was given a timeout of 1000 seconds.



 §.§ Results


We present scatter plots demonstrating the behavior of satisfiability of k-CNF-XOR formulas. 
For lack of space, we present results only for three experiments[
	The data from all experiments is available at <http://www.cs.rice.
	edu/CS/Verification/Projects/CUSP/>
].
The plots for k=2,3 and 5
are shown in Figure <ref>, <ref>, and  <ref>
 respectively. The value of n is set to 150, 100, and 50 respectively for the three experiments above. 

Each figure is a 2D plot, representing the observed probability that  is 
satisfiable as the density of k-clauses r and the density of XOR-clauses s varies. 
The x-axis indicates the density of k-clauses r. The y-axis indicates the density of XOR-clauses s. 
The dark (respectively, light) regions represent clause densities where almost all (respectively, no) sampled formulas were satisfiable.

Note that  consists only of XOR clauses when r=0. Examining the figures along the line r=0 the phase-transition location is 
around (r=0, s=1), which matches previous theoretical results on the phase-transition for XOR formulas <cit.>. 
Likewise, [xorNum=0] = and, by examining the figures along the line s=0, we observe phase-transition 
locations that match previous studies on the phase-transition 
for k-CNF formulas for k=2,3, and 5  <cit.>. Note that the phase-transition we observe for 2-CNF formulas is slightly above the true location at s=1 <cit.>; the correct phase-transition point for 2-CNF formulas is observed only when the number of variables is above 4096 <cit.>.




In all the plots, we observe a large triangular region where the probability that  is 
satisfiable is nearly 1. We likewise observe a 
separate region where the observed probability that  is satisfiable is nearly 0. 
More surprisingly, the shared boundary between the two regions for large areas of the 
plots seems to be a constant-slope line. A closer examination of this line at the bottom-right corners of the figures for k=2 and k=3, where the k-clause density is large, reveals that the line appears to “kink” and abruptly change slope. We discuss this further in Section <ref>.



§ ESTABLISHING A PHASE-TRANSITION
 
The experimental results presented in Section <ref> empirically demonstrate the existence of a  k-CNF-XOR phase-transition. Theorem <ref> shows that the k-CNF-XOR phase-transition exists when the density of k-clauses is small. In particular, the function ϕ_k(r) (defined in Lemma <ref>) gives the location of a phase-transition between a region of satisfiability and a region of unsatisfiability in random k-CNF-XOR formulas.



	
	Let k ≥ 2.	There is a function ϕ_k(r), a constant α_k ≥ 1, and a countable set of real numbers 𝒞_k (all defined in Lemma <ref>) such that for all r ∈ [0, α_k) \𝒞_k and s ≥ 0:
	
		
  *  If s < ϕ_k(r), then w.h.p.  is satisfiable.
		
  *  If s > ϕ_k(r), then w.h.p.  is unsatisfiable.
	


	Part <ref> follows directly from Lemma <ref>. Part <ref> follows directly from Lemma <ref>. The proofs of these lemmas are presented in Sections <ref> and <ref> respectively.


ϕ_k(r) is the free-entropy density of k-CNF, drawing on concepts from spin-glass theory <cit.>. From the expression for ϕ_k(r) in Lemma <ref>, it is easily verified that ϕ_k(0) = 1 and that ϕ_k(r) is a monotonically decreasing function of r. Thus when the k-clause density (r) is 0, Theorem <ref> says that an XOR-clause density of 1 is a phase-transition for XOR-formulas, matching previously known results <cit.>. As the k-clause density increases, ϕ(r) is decreasing and so the XOR-clause density required to reach the phase-transition decreases.

Theorem <ref> fully characterizes the random satisfiability of  when r < 1. In the case k=2, prior results on random 2-CNF satisfiability characterize the rest of the region. If r > 1, then [k=2] is unsatisfiable w.h.p. <cit.> and so the 2-clauses within [k=2] are unsatisfiable w.h.p. without considering the XOR-clauses. Therefore [k=2] is unsatisfiable w.h.p. if r > 1. This, together with Theorem <ref>, proves that ϕ_2(r) is the complete location of the 2-CNF-XOR phase-transition.

Moreover, Lemma <ref> shows that α_k ≥ (1 - o_k(1)) · 2^k ln(k) / k (where o_k(1) denotes a term that converges to 0 as k →∞) and so Theorem <ref> shows that a phase-transition exists until near r = 2^k ln(k) / k for sufficiently large k.

For small k ≥ 3, the region r < 1 characterized by Theorem <ref> is only a small portion of the region where the subset of k-clauses remains satisfiable. Moreover, the location of the phase-transition ϕ_k(r) given by Theorem <ref> is difficult to compute directly. Theorem <ref> gives explicit lower and upper bounds on the location of a phase-transition region.


 
	Let k ≥ 3. There is a function  (defined in Lemma <ref>)
	such that for all s ≥ 0 and r ≥ 0:	
	
		
  *  If s < 1/2log_2() and r < 2^k ln(2) - 1/2((k+1)ln(2) + 3), then w.h.p.  is satisfiable.
		
  *  If s > r log_2(1 - 2^-k) + 1, then w.h.p.  is unsatisfiable.
	


	Part <ref> follows directly from Lemma <ref>. Part <ref> follows directly from Lemma <ref>. The proofs of these lemmas are presented in Sections <ref> and <ref> respectively.


Both the upper bound r log_2(1 - 2^-k) + 1 and (using the expression for  in Lemma <ref>) the lower bound 1/2log_2() are linear in r. 
When the k-clause density r is 0, Theorem <ref> agrees with Theorem <ref>. As the k-clause density increases past Θ(2^k), Theorem <ref> no longer gives a lower bound on the location of a possible phase-transition.





 §.§ A Proof of the Lower Bound


We now establish Theorem <ref>.<ref> and Theorem <ref>.<ref>, which follow directly from Lemma <ref> and Lemma <ref> respectively. 

The key idea in the proof of these lemmas is to decompose  into independently generated k-CNF and XOR formulas, so that =. We can then bound the number of solutions to  from below with high probability and bound from below the probability that  becomes unsatisfiable after including XOR-clauses on top of . 

The following three lemmas achieve the first of the two tasks. The first, Lemma <ref>, gives a tight bound on # for small k-clause densities.

	
	Let k ≥ 2 and let α_k be the supremum of {r : ∃δ > 0 s.t. ( is unsat.) ≤ O(1/(log n)^1+δ)}. Then α_k ≥ 1. Furthermore, there exists a countable set of real numbers 𝒞_k such that for all r ∈ [0, α_k) \𝒞_k:
	
		
  *  The sequence 1/nlog_2(#) |  is sat. converges to a limit as n →∞. Let ϕ_k(r) be this limit.
		
  *  For all ϵ > 0, w.h.p. (2^ϕ_k(r)-ϵ)^n ≤#.
		
  *  For all ϵ > 0, w.h.p. (2^ϕ_k(r)+ϵ)^n ≥#.
	


	These proofs are given in <cit.>. α_k ≥ 1 is given as Remark 2. Part (a) is given as Theorem 3. Parts (b) and (c) are given as Theorem 1.


We abuse notation to let ϕ_k(r) denote the limit of the sequence in Lemma <ref>.<ref> for all r > 0, although a priori this sequence may not converge for r ≥α_k. Later work refined the value of α_k in Lemma <ref> for sufficiently large k and so extended the tight bound on #. In particular, Lemma <ref> implies that α_k ≥ (1 - o_k(1)) · 2^k ln(k) / k.

	
	Let k ≥ 2. For all r ≥ 0, if r ≤ (1 - o_k(1)) · 2^k ln(k) / k then ( is sat.) ≥ 1 - O(1/n).


	The proof of this is given as Theorem 1.3 of <cit.>.



It is difficult to compute ϕ_k(r) directly. Instead, Lemma <ref> provides a weaker but explicit lower bound on #.

	
	Let k ≥ 3, ϵ > 0, and r ≥ 0. Let β_k be the smallest positive solution to β_k (2-β_k)^k-1 = 1 and define = 4 (((1 - β_k /2)^k - 2^-k)^2 / (1-β_k)^k)^r.
	
	If r < 2^k ln(2) - 1/2((k+1)ln(2) + 3),
	then w.h.p. 1/2( - ϵ)^n/2≤#.


	The proof of this is given on page 264 of <cit.> within Section 6 (Proof of Theorem 6); the definition of  is given as equation (20).


Before we analyze how the solution space of  interacts with the solution space of , we must characterize the solution space of . The following lemma shows that the solutions of  are pairwise independent, meaning that a single satisfying assignment of  gives no information on other satisfying assignments.

	
	Let n ≥ 0 and s ≥ 0. If σ and σ' are distinct assignments of truth values to the variables {X_1, ⋯, X_n}:
	
		
  * (σ satisfies ) = 2^-sn
		
  * (σ satisfies  | σ' satisfies ) = 2^-sn
	


	The proof of this is given in the proof of Lemma 1 of <cit.>.


The following lemma bounds from below the probability that a formula H (in Lemma <ref> we take H =) remains satisfiable after including XOR-clauses on top of H. This result and proof is similar to Corollary 3 from  <cit.>.

	
	Let α≥ 1, s ≥ 0, n ≥ 0, and let H be a formula defined over {X_1, ⋯, X_n}.
	Then
	(H  is satisfiable | # H ≥ 2^sn + α) ≥ 1 - 2^-α.


	Let R be the set of all truth assignments to the variables in X that satisfy H; there are #H such truth assignments. For every truth assignment σ∈ R, let Y_σ be a 0-1 random variable that is 1 if σ satisfies H and 0 otherwise. Note that Y_σ = Y_σ^2 - Y_σ^2 ≤Y_σ^2. Since Y_σ is a 0-1 random variable, Y_σ^2 = Y_σ and thus Y_σ≤Y_σ.
	
	Let σ and σ' be distinct truth assignments in R. By Lemma <ref>, 	Y_σ Y_σ' = Y_σY_σ' = 2^-sn· 2^-sn. Thus Y_σY_σ' = Y_σ Y_σ' - Y_σY_σ' = 0.
	
	Let the random variable Y be the number of solutions to H, so Y = # (H ) = ∑_σ Y_σ. Thus Y = ∑_σ Y_σ = ∑_σY_σ + ∑_σ≠σ'Y_σY_σ'. Since the covariance of Y_σ and Y_σ' is 0 for all pairs of distinct truth assignments σ and σ' in R, we get that Y = ∑_σY_σ. Since Y_σ≤Y_σ for all truth assignments σ in R, we get that Y≤∑_σY_σ. Since Y = ∑_σ Y_σ = ∑_σY_σ, we conclude that Y≤Y. Moreover, since Y_σ = (σ satisfies ) = 2^-sn we get Y = # H · 2^-sn.
	
	Let the event E_n denote that H is unsatisfiable. Thus if E_n occurs then then Y=0 and so |Y - Y| ≥Y. This implies that ( E_n) ≤(|Y - Y| ≥Y). Chebyshev's inequality says that (|Y- Y| ≥Y) ≤Y / Y^2. It follows that ( E_n) ≤Y / Y^2. Since Y≤Y, we get that ( E_n) ≤Y^-1. Therefore by plugging in the value for Y we get ( E_n) ≤ (# H)^-1· 2^sn. 
	
	Finally, if we assume that #H ≥ 2^sn + α then (# H)^-1· 2^sn≤ 2^-α. Therefore ( E_n  | #H ≥ 2^sn + α) ≤ 2^-α.


Using the key behavior of XOR-clauses described in Lemma <ref>, we can transform lower bounds (w.h.p.) on the number of solutions to  into lower bounds on the location of a possible k-CNF-XOR phase-transition.

	
	Let k ≥ 2, s ≥ 0, and r ≥ 0. Let B_1, B_2, ⋯ be an infinite convergent sequence of positive real numbers such that B_i^n ≤# occurs w.h.p. for all i ≥ 1. If s < log_2(lim_i →∞ B_i), then w.h.p.  is satisfiable.


	For all integers n ≥ 0, let the event E_n denote the event when  is satisfiable. We would like to show that (E_n) converges to 1 as n →∞. 
	
	The general idea of the proof follows. We first decompose  as =. Let the event L_n denote the event when the number of solutions of  is bounded from below (by a lower bound to be specified later). We show that L_n occurs w.h.p.. Next, we use Lemma <ref> to bound from below the probability that  remains satisfiable given that  has enough solutions; we use this to show that (E_n | L_n) converges to 1 as n →∞. Finally, we combine these results to prove that (E_n) converges to 1.
	
	Since 2^s < lim_i →∞ B_i, there is some integer i ≥ 1 such that 2^s < B_i. Define the event L_n as the event when #≥ B_i^n. Then L_n occurs w.h.p. by hypothesis.
	
	Next, we show that (E_n | L_n) converges to 1. Choose δ > 0 and N > 0 such that 2^s + δ + 1/N < B_i; we can always find sufficiently small δ and sufficiently large N such that this holds. Since we are concerned only with the behavior of (E_n  |  L_n) in the limit, we can restrict our attention only to large enough n. In particular, consider n > 2N. Then we get that 2^sn + δ n + 2 < B_i^n and so 2^sn + δ n + 1 < B_i^n. Let α = δ n + 1, so that 2^sn + α≤ B_i^n. Then Lemma <ref> says that (E_n  |  L_n) ≥ 1 - 2^-δ n -1. Since 1 - 2^-δ n - 1 converges to 1 as n →∞, (E_n  |  L_n) must also converge to 1.
	
	Thus both (E_n  |  L_n) and (L_n) converge to 1 as n →∞. Since (E_n ∩ L_n) = (E_n | L_n) ·(L_n), this implies that (E_n ∩ L_n) also converges to 1. Since (E_n ∩ L_n) ≤(E_n) ≤ 1, this implies that (E_n) converges to 1.


Finally, it remains only to use Lemma <ref> to obtain bounds on the k-CNF-XOR phase-transition. The tight lower bound on # from Lemma <ref>.<ref> corresponds to a tight lower bound on the location of the phase-transition.

	
	Let k ≥ 2, and let α_k, 𝒞_k, and ϕ_k(r) be as defined in Lemma <ref>. 
	For all r ∈ [0, α_k) \𝒞_k and s ∈ [0, ϕ_k(r)),  is satisfiable w.h.p..


	Let B_i = 2^ϕ_k(r)-1/i. By Lemma <ref>.<ref>, B_i^n ≤# w.h.p. for all i ≥ 1. Furthermore, lim_i →∞ B_i = 2^ϕ_k(r) and so s < log_2(lim_i →∞ B_i). Thus  is satisfiable w.h.p. by Lemma <ref>.


The weaker lower bound on # from Lemma <ref> corresponds to a weaker lower bound on the location of the phase-transition.

	
	Let k ≥ 3, s ≥ 0, and r ≥ 0. If r < 2^k ln(2) - 1/2(k+1)ln(2) + 3/2 and s < 1/2log_2(), then  is satisfiable w.h.p..


	Let B_i = ( - 1/i)^1/2. This is an increasing sequence in i, so log_2(B_i+1 / B_i) is positive for all i ≥ 1. Consider one such i ≥ 1 and define N_i = 1 / log_2(B_i+1 / B_i). Then for all n > N_i it follows that 2^1/n < B_i+1 / B_i and so B_i^n < 1/2 B_i+1^n. By Lemma <ref>, 1/2B_i+1^n ≤# w.h.p. and therefore B_i^n < 1/2 B_i+1^n ≤# w.h.p. as well.
		
	 Furthermore, lim_i →∞ B_i = ^1/2 and so s < log_2(lim_i →∞ B_i). Thus  is satisfiable w.h.p. by Lemma <ref>.




 §.§ A Proof of the Upper Bound



We now establish Theorem <ref>.<ref> and Theorem <ref>.<ref>, which follow directly from Lemma <ref> and Lemma <ref> respectively. 

Similar to Section <ref>, the key idea in the proof of these lemmas is to decompose  into independently generated k-CNF and XOR formulas, so that =. We can then bound the number of solutions to  from above with high probability and bound from below the probability that  becomes unsatisfiable after including XOR-clauses on top of .

The first of these two tasks is accomplished through Lemma <ref>.<ref>, which gives a tight upper bound on # for small k-clause densities, and by Lemma <ref>, which gives a weaker explicit upper bound on #.

	
	For all ϵ > 1, k ≥ 2, and r ≥ 0, w.h.p. # < (2 ϵ· (1 - 2^-k)^r)^n.


	Let X = #.	For a random assignment on n variables σ, note that (σ satisfies [cnfNum=1]) = (1 - 2^-k). Since the rn k-clauses of  were chosen independently, this implies that X = 2^n (1 - 2^-k)^rn. 
	
	By Markov's inequality, we get (X ≥ϵ^n X) ≤X / (ϵ^n X) = ϵ^-n.
	Since 1 - 2^-k < 1 and so 2^n ϵ^n (1 - 2^-k)^rn≤ 2^n ϵ^n (1 - 2^-k)^rn, it follows that (X ≥ϵ^n 2^n (1 - 2^-k)^rn) ≤(X ≥ϵ^n X) ≤ϵ^-n. Thus lim_n →∞(X < ϵ^n 2^n (1 - 2^-k)^rn) = 1.



The following lemma bounds from below the probability that a formula H (in Lemma <ref> we take H =) remains satisfiable after including XOR-clauses on top of H. This result and proof is similar to Corollary 1 from <cit.>.

	
	Let α≥ 1, s ≥ 0, n ≥ 0, and let H be a formula defined over X = {X_1, ⋯, X_n}. Then 
	(H  is unsatisfiable | #H ≤ 2^sn - α) ≥ 1 - 2^-α.


	Let the random variable Y denote # (H ) as in Lemma <ref>. Markov's inequality implies that (Y ≥ 1) ≤Y. Recall from Lemma <ref> that Y =# H · 2^-sn, so (Y ≥ 1) ≤# H · 2^-sn. If #H ≤ 2^sn - α, then # H · 2^-sn≤ 2^-α. Thus (Y ≥ 1  | #H ≤ 2^sn - α) ≤ 2^-α. Since H is unsatisfiable exactly when Y = 0, we conclude  (H  is unsatisfiable) ≥ 1 - 2^-α.


Using the key behavior of XOR-clauses described in Lemma <ref>, we can transform upper bounds (w.h.p.) on the number of solutions to  into upper bounds on the location of a possible k-CNF-XOR phase-transition.


Let k ≥ 2, s ≥ 0, and r ≥ 0. Let B_1, B_2, ⋯ be an infinite convergent sequence of positive real numbers such that #≤ B_i^n occurs w.h.p. for all i ≥ 1. If s > log_2(lim_i →∞ B_i), then w.h.p.  is unsatisfiable.


	For all integers n ≥ 0, let the event E_n denote the event when  is unsatisfiable. We would like to show that ( E_n) converges to 1 as n →∞. 
	
	The general idea of the proof follows. Note that = as in Lemma <ref>. Let the event U_n denote the event when the number of solutions of  is bounded from above (by an upper bound to be specified later). We show that U_n occurs w.h.p.. Next, we use Lemma <ref> to bound from below the probability that  becomes unsatisfiable given that  has few solutions; we use this to show that ( E_n  |  U_n) converges to 1 as n →∞. Finally, we combine these results to prove that ( E_n) converges to 1.
			
	Since 2^s > lim_i →∞ B_i, there is some integer i ≥ 1 such that 2^s > B_i. Define the event U_n as the event when #≤ B_i^n. Then U_n occurs w.h.p. by hypothesis.
	
	Next, we show that ( E_n | U_n) converges to 1. Choose δ > 0 and N > 0 such that 2^s - δ - 1/N > B_i. As in Lemma <ref> we are concerned only with the behavior of ( E_n | U_n) in the limit so we can restrict our attention only to large enough n. In particular, consider n > N. Then we get that 2^sn - δ n - 1 > 2^sn - δ n - n/N > B_i^n. Let α = δ n + 1, so that 2^sn - α≥ B_i^n. Then Lemma <ref> says that ( E_n  |  U_n) ≥ 1 - 2^-δ n - 1. Since 1 - 2^-δ n - 1 converges to 1 as n →∞, ( E_n  |  U_n) must also converge to 1. 
	
	Thus both ( E_n | U_n) and (U_n) converge to 1 as n →∞. Since ( E_n ∩ U_n) = ( E_n  |  U_n) ·(U_n), this implies that ( E_n ∩ U_n) also converges to 1. Since ( E_n ∩ U_n) ≤( E_n) ≤ 1, this implies that ( E_n) converges to 1.


Finally, it remains only to use Lemma <ref> to obtain bounds on the k-CNF-XOR phase-transition. The tight upper bound on # from Lemma <ref>.<ref> corresponds to a tight upper bound on the location of the phase-transition.

	
	
	Let k ≥ 2, and let α_k, 𝒞_k, and ϕ_k(r) be as defined in Lemma <ref>. 
	Then for all r ∈ [0, α_k) \𝒞_k and s > ϕ_k(r),  is unsatisfiable w.h.p..


	Let B_i = 2^ϕ_k(r)+1/i. By Lemma <ref>.<ref>, B_i^n ≥# w.h.p. for all i ≥ 1. Furthermore, lim_i →∞ B_i = 2^ϕ_k(r) and so s > log_2(lim_i →∞ B_i). Thus  is unsatisfiable w.h.p. by Lemma <ref>.


The weaker upper bound on # from Lemma <ref> corresponds to a weaker upper bound on the phase-transition.

	
	Let k ≥ 2, s ≥ 0, and r ≥ 0. If s > 1 + r log_2(1 - 2^-k), then  is unsatisfiable w.h.p..


	Let B_i = ((1 + 1/i) · 2(1 - 2^-k)^r). By Lemma <ref>, B_i^n ≥# w.h.p. for all i ≥ 1. Furthermore, lim_i →∞ B_i = 2(1 - 2^-k)^r and so s > log_2(lim_i →∞ B_i). Thus  is unsatisfiable w.h.p. by Lemma <ref>.




§ EXTENDING THE PHASE-TRANSITION REGION



Section <ref> proved that a phase-transition exists for k-CNF-XOR formulas when the k-clause density is small. Our empirical observations in Section <ref> suggest that a phase-transition exists for higher k-clause densities as well. 
Moreover, we observed a phase-transition that follows a linear trade-off between k-clauses and XOR-clauses.
In this section, we conjecture two possible extensions to our theoretical results.

The first extension follows from Theorem <ref>, which implies that s = ϕ_k(r) gives the location of the phase-transition for small k-clause densities. It is thus natural to conjecture that ϕ_k(r) gives the location of the k-CNF-XOR phase-transition for all (except perhaps countably many) r > 0. This would follow from a conjecture of <cit.>.

The second extension follows from the experimental results in Section <ref>, which suggest that the location of the phase-transition follows a linear trade-off between k-clauses and XOR-clauses. This leads to the following conjecture:

	Let k ≥ 2. Then there exists a slope L_k < 0 and a constant α_k^* > 0 such that for all r ∈ [0, α_k^*) and s ≥ 0:
	
		
  * If s < r L_k + 1, then w.h.p.  is satisfiable.
		
  * If s > r L_k + 1, then w.h.p.  is unsatisfiable.
	


Theorem <ref> bounds the possible values for L_k. Moreover, if the Linear k-CNF-XOR Phase-Transition Conjecture holds, then Theorem <ref> implies that ϕ_k(r) is linear for all r < α_k and r < α_k^*. Explicit computations of ϕ_k(r) (or sufficiently tight bounds) would resolve this conjecture.

Note that this conjecture does not necessarily describe the entire k-CNF-XOR phase-transition; a phase-transition may exist when r > α_k^* as well. The experimental results in Section <ref> for k = 2 and k = 3 suggest that the location of the phase-transition may “kink” and become non-linear for large enough k-clause densities. We leave the full characterization of the k-CNF-XOR phase-transition for future work, noting that a full characterization would resolve the Satisfiability Phase-Transition Conjecture.



§ CONCLUSION
 
We presented the first study of phase-transition phenomenon in the satisfiability of k-CNF-XOR random formulas. We showed that the free-entropy density ϕ_k(r) of k-CNF formulas gives the location of the phase-transition for k-CNF-XOR formulas when the density of the k-CNF clauses is small. We conjectured in the k-CNF-XOR Linear Phase-Transition Conjecture that this phase-transition is linear. We leave further analysis and proof of this conjecture for future work.

Pittel and Sorkin <cit.> recently identified the location of the phase-transition for random ℓ-XOR formulas, where each clause contains exactly ℓ literals. This suggests that a phase-transition may also exist in formulas that mix k-CNF clauses together with ℓ-XOR clauses.

In this work we did not explore the runtime of  solvers over the space of k-CNF-XOR formulas. Historically, other phase-transition phenomena have been closely connected empirically to solver runtime. Developing this connection in the case of k-CNF-XOR formulas is an exciting direction for future research and may lead to practical improvements to hashing-based sampling and counting algorithms.



 §.§ Acknowledgments

 The authors would like to thank Dimitris Achlioptas for helpful discussions in the early stages of this project.
 
Work supported in part by NSF grants CCF-1319459 and IIS-1527668, by NSF Expeditions in Computing project “ExCAPE: Expeditions in Computer Augmented Program Engineering", by BSF grant 9800096,  by the Ken Kennedy Institute Computer Science & Engineering
 Enhancement Fellowship funded by the Rice Oil & Gas HPC Conference, and Data Analysis and 
 Visualization Cyberinfrastructure funded by NSF under grant 
 OCI-0959097. Part of this work was done during a visit to the Israeli Institute for Advanced Studies.
 


[Abbe and Montanari2014]AM14
E. Abbe and A. Montanari.
On the concentration of the number of solutions of random
  satisfiability formulas.
Random Structures & Algorithms, 45(3):362–382, 2014.

[Achlioptas and Coja-Oghlan2008]AchCoj08
D. Achlioptas and A. Coja-Oghlan.
Algorithmic barriers from phase transitions.
In Proc. of FoCS, pages 793–802, 2008.

[Achlioptas et al.2011]ACR11
D. Achlioptas, A. Coja-Oghlan, and F. Ricci-Tersenghi.
On the solution-space geometry of random constraint satisfaction
  problems.
Random Structures & Algorithms, 38(3):251–268, 2011.

[Achlioptas2009]Achlioptas09
D. Achlioptas.
Random satisfiability.
In Handbook of Satisfiability, pages 245–270. IOS Press, 2009.

[Apt2003]Apt03
K. Apt.
Principles of Constraint Programming.
Cambridge Univ. Press, 2003.

[Belov et al.2014]BDHJ14
A. Belov, D. Diepold, M. J. Heule, and M. Järvisalo.
Sat competition 2014.
2014.

[Chakraborty et al.2013a]CMV13a
S. Chakraborty, K. S. Meel, and M. Y. Vardi.
A scalable and nearly uniform generator of SAT witnesses.
In Proc. of CAV, pages 608–623, 2013.

[Chakraborty et al.2013b]CMV13b
S. Chakraborty, K. S. Meel, and M. Y. Vardi.
A scalable approximate model counter.
In Proc. of CP, pages 200–216, 2013.

[Chakraborty et al.2014a]CFMSV14
S. Chakraborty, D. J. Fremont, K. S. Meel, S. A. Seshia, and M. Y. Vardi.
Distribution-aware sampling and weighted model counting for SAT.
In Proc. of AAAI, pages 1722–1730, 2014.

[Chakraborty et al.2014b]CMV14
S. Chakraborty, K. S. Meel, and M. Y. Vardi.
Balancing scalability and uniformity in SAT witness generator.
In Proc. of DAC, pages 1–6, 2014.

[Chakraborty et al.2016]CMV16
S. Chakraborty, K. S. Meel, and M. Y. Vardi.
Algorithmic improvements in approximate counting for probabilistic
  inference: From linear to logarithmic SAT calls.
In Proc. of IJCAI, 2016.

[Cheeseman et al.1991]CKT91
P. Cheeseman, B. Kanefsky, and W. M. Taylor.
Where the really hard problems are.
In Proc. of IJCAI, pages 331–340, 1991.

[Chvátal and Reed1992]CR92
V. Chvátal and B. Reed.
Mick gets some (the odds are on his side).
In Proc. of FoCS, pages 620–627, 1992.

[Coarfa et al.2003]CDSSV03
C. Coarfa, D. D. Demopoulos, A. S. M. Aguirre, D. Subramanian, and M. Y. Vardi.
Random 3-sat: The plot thickens.
Constraints, 8(3):243–261, 2003.

[Coja-Oghlan and Panagiotou2013]CP13a
A. Coja-Oghlan and K. Panagiotou.
Going after the k-sat threshold.
In Proc. of SToC, pages 705–714, 2013.

[Coja-Oghlan and Reichman2013]CR13
A. Coja-Oghlan and D. Reichman.
Sharp thresholds and the partition function.
In Journal of Physics: Conference Series, volume 473, page
  012015, 2013.

[Crawford and Auton1993]CA93
J. M. Crawford and L. D. Auton.
Experimental results on the crossover point in satisfiability
  problems.
In Proc. of AAAI, pages 21–27, 1993.

[Creignou and Daudé1999]CD99
N. Creignou and H. Daudé.
Satisfiability threshold for random xor-cnf formulas.
Discrete Applied Mathematics, 96–97:41 – 53, 1999.

[Creignou and Daudé2003]CD03
N. Creignou and H. Daudé.
Smooth and sharp thresholds for random k-xor-cnf satisfiability.
RAIRO:ITA, 37(2):127–147, 2003.

[Dechter and Meiri1994]DM94
R. Dechter and I. Meiri.
Experimental evaluation of preprocessing algorithms for constraint
  satisfaction problems.
Artificial Intelligence, 68:211–241, 1994.

[Dechter2003]Dec03
R. Dechter.
Constraint Processing.
Morgan Kaufmman, 2003.

[Ding et al.2015]DSS15
J. Ding, A. Sly, and N. Sun.
Proof of the satisfiability conjecture for large k.
In Proc. of SToC, pages 59–68. ACM, 2015.

[Dubois and Mandler2002]DM02
O. Dubois and J. Mandler.
The 3-xorsat threshold.
Comptes Rendus Mathematique, 335(11):963 – 966, 2002.

[Goerdt1996]Goerdt96
A. Goerdt.
A threshold for unsatisfiability.
Journal of Computer and System Sciences, 53(3):469 – 486,
  1996.

[Gogioso2014]Gogioso14
S. Gogioso.
Aspects of statistical physics in computational complexity.
arXiv:1405.3558, 2014.

[Gomes et al.2006]GSS06
C. P. Gomes, A. Sabharwal, and B. Selman.
Model counting: A new strategy for obtaining good bounds.
In Proc. of AAAI, volume 21, pages 54–61, 2006.

[Gomes et al.2007]GSS07
C. P. Gomes, A. Sabharwal, and B. Selman.
Near-uniform sampling of combinatorial spaces using XOR
  constraints.
In Proc. of NIPS, pages 670–676, 2007.

[Ivrii et al.2015]IMMV15
A. Ivrii, S. Malik, K. Meel, and M. Vardi.
On computing minimal independent support and its applications to
  sampling and counting.
Constraints, pages 1–18, 2015.

[Kirkpatrick and Selman1994]KS94
S. Kirkpatrick and B. Selman.
Critical behavior in the satisfiability of random boolean
  expressions.
Science, 264(5163):1297–1301, 1994.

[Meel et al.2016]MVCFSFIM16
K. S. Meel, M. Vardi, S. Chakraborty, D. J. Fremont, S. A. Seshia, D. Fried,
  A. Ivrii, and S. Malik.
Constrained sampling and counting: Universal hashing meets sat
  solving.
In Proc. of Beyond NP Workshop, 2016.

[Mitchell et al.1992]MSL92
D. Mitchell, B. Selman, and H. Levesque.
Hard and easy distributions of sat problems.
In Proc. of AAAI, pages 459–465, 1992.

[Mu and Hoos2015]MH15
Z. Mu and H. H. Hoos.
On the empirical time complexity of random 3-sat at the phase
  transition.
In Proc. of IJCAI, pages 367–373, 2015.

[Pittel and Sorkin2015]PS15
B. Pittel and G. B. Sorkin.
The satisfiability threshold for k-xorsat.
Combinatorics, Probability and Computing, FirstView:1–33, 10
  2015.

[Soos et al.2009]SNC09
M. Soos, K. Nohl, and C. Castelluccia.
Extending SAT Solvers to Cryptographic Problems.
In Proc. of SAT. Springer-Verlag, 2009.

[Wilson2000]Wilson2000
D. B. Wilson.
Random 2-sat data.
http://dbwilson.com/2sat-data/, 2000.


