Speaker: Dr. Kuldeep Meel

Date and Venue: Wednesday 13th September 2017, 12:00 - 13:00, SIT Building Seminar Room (Room 001).

Title: On Demystifying CNF-XOR Formulas


Abstract: 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.

Speaker Bio: Kuldeep Meel is starting as Assistant Professor at National University of Singapore. His research broadly lies at the intersection of artificial intelligence and formal methods. He is the recipient of a 2016-17 IBM PhD Fellowship, the 2016-17 Lodieska Stockbridge Vaughn Fellowship and the 2014 Vienna Center of Logic and Algorithms International Outstanding Masters thesis award.