I am a fifth 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:
ADDMC: Weighted Model Counting with Algebraic Decision Diagrams
Proceedings of ThirtyFourth AAAI Conference on Artificial Intelligence (AAAI), 2020.
We present an algorithm to compute exact literalweighted model counts of Boolean formulas in Conjunctive Normal Form. Our algorithm employs dynamic programming and uses Algebraic Decision Diagrams as the primary data structure. We implement this technique in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We then compare ADDMC to stateoftheart exact weighted model counters (Cachet, c2d, d4, and miniC2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver.

Transformations of Boolean Functions
Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2019.
Boolean functions are characterized by the unique structure of their solution space. Some properties of the solution space, such as the possible existence of a solution, are well sought after but difficult to obtain. To better reason about such properties, we define transformations as functions that change one Boolean function to another while maintaining some properties of the solution space. We explore transformations of Boolean functions, compactly described as Boolean formulas, where the property is to maintain is the number of solutions in the solution spaces. We first discuss general characteristics of such transformations. Next, we reason about the computational complexity of transforming one Boolean formula to another. Finally, we demonstrate the versatility of transformations by extensively discussing transformations of Boolean formulas to "blocks," which are solution spaces in which the set of solutions makes a prefix of the solution space under a lexicographic order of the variables.

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.
