Rice University

Events at Rice

Thesis Defense

Graduate and Postdoctoral Studies
Computer Science

Speaker: Jeffrey Dudek
Masters Candidate

Random CNF-XOR Formulas

Tuesday, April 18, 2017
9:00 AM  to 11:00 AM

1049  Duncan Hall

The Boolean-Satisfaction Problem (SAT) is fundamental in many diverse areas such as artificial intelligence, formal verification, and biology. A large body of work explains the runtime performance of modern SAT solvers through analysis of random k-CNF formulas. Recent universal-hashing based approaches to the problems of sampling and counting crucially depend on the runtime performance of specialized SAT solvers on formulas expressed as the conjunction of both k-CNF constraints and variable-width XOR constraints (known as CNF-XOR formulas), but random CNF-XOR formulas are unexplored in prior work. In this work, we present the first study of random CNF-XOR formulas. We show empirical evidence of a surprising phase-transition in the satisfiability of random CNF-XOR formulas that follows a linear trade-off between k-CNF and XOR constraints. Moreover, we prove that a phase-transition in the satisfiability of random CNF-XOR formulas exists for k=2 and (when the number of k-CNF constraints is small) for k>2. We empirically demonstrate that a state-of-the-art SAT solver scales exponentially on random CNF-XOR formulas across a wide range of XOR-clause densities, peaking around the empirical phase-transition location. Finally, we prove that the solution space of random CNF-XOR formulas 'shatters' at all nonzero XOR-clause densities into well-separated components.

<<   July 2017   >>
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30 31

Search for Events