I am a fourth year PhD student in the Department of Computer Science at Rice University, advised by Prof. Moshe Vardi. I obtained a BS in Computer Science and a BA in Mathematics from Rice University as well.
My research interests are in:
Random CNFXOR Formulas
Masters Thesis, Rice University, April 2017. Boolean Satisfiability (SAT) is fundamental in many diverse areas such as artificial intelligence, formal verification, and biology. Recent universalhashing 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 kCNF constraints and variablewidth XOR constraints (known as CNFXOR formulas), but random CNFXOR formulas are unexplored in prior work. In this work, we present the first study of random CNFXOR formulas. We prove that a phasetransition in the satisfiability of random CNFXOR formulas exists for k=2 and (when the number of kCNF constraints is small) for k>2. We empirically demonstrate that a stateoftheart SAT solver scales exponentially on random CNFXOR formulas across many clause densities, peaking around the empirical phasetransition location. Finally, we prove that the solution space of random CNFXOR formulas 'shatters' at all nonzero XORclause densities into wellseparated components.

The Hard Problems Are Almost Everywhere For Random CNFXOR Formulas
Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2017.
Recent universalhashing based approaches to sampling and counting crucially depend on the runtime performance of SAT solvers on formulas expressed as the conjunction of both CNF constraints and variablewidth XOR constraints (known as CNFXOR formulas). In this paper, we present the first study of the runtime behavior of SAT solvers equipped with XORreasoning techniques on random CNFXOR formulas. We empirically demonstrate that a stateoftheart SAT solver scales exponentially on random CNFXOR formulas across a wide range of XORclause densities, peaking around the empirical phasetransition location. On the theoretical front, we prove that the solution space of a random CNFXOR formula 'shatters' at all nonzero XORclause densities into wellseparated components, similar to the behavior seen in random CNF formulas known to be difficult for many SAT algorithms.

Combining the kCNF and XOR PhaseTransitions
Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2016.
The runtime performance of modern SAT solvers on random kCNF formulas is deeply connected with the `phasetransition' phenomenon seen empirically in the satisfiability of random kCNF formulas. Recent universal hashingbased approaches to sampling and counting crucially depend on the runtime performance of SAT solvers on formulas expressed as the conjunction of both kCNF and XOR constraints (known as kCNFXOR formulas), but the behavior of random kCNFXOR formulas is unexplored in prior work. In this paper, we present the first study of the satisfiability of random kCNFXOR formulas. We show empirical evidence of a surprising phasetransition that follows a linear tradeoff between kCNF and XOR constraints. Furthermore, we prove that a phasetransition for kCNFXOR formulas exists for k = 2 and (when the number of kCNF constraints is small) for k > 2.
