Jeffrey Dudek

I am a third 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:
  • Machine Learning
  • Constrained Counting and Sampling
  • SAT Solving and Phase-Transition Phenomena
  • Awards and Distinctions

  • Ken Kennedy Institute - Cray Inc. Graduate Fellowship, 2017 – 2018
  • NSF Graduate Research Fellowship (Honorable Mention), 2017
  • Ken Kennedy Institute Enhancement Fellowship, 2015 – 2019
  • Trustee and LJ Walsh Scholarships, awarded by Rice University, 2011 – 2015
  • Thomas J. Watson Memorial Scholarship, awarded by IBM, 2011 – 2015
  • Zevi & Bertha Salsberg Award, awarded by Will Rice College, 2012
  • Publications

    Random CNF-XOR Formulas
    Jeffrey M. Dudek
    Masters Thesis, Rice University, April 2017.
    Boolean Satisfiability (SAT) is fundamental in many diverse areas such as artificial intelligence, formal verification, and biology. 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 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 many 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.
    The Hard Problems Are Almost Everywhere For Random CNF-XOR Formulas
    Jeffrey M. Dudek, Kuldeep S. Meel, and Moshe Y. Vardi
    Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2017.
    Recent universal-hashing 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 variable-width XOR constraints (known as CNF-XOR formulas). In this paper, we present the first study of the runtime behavior of SAT solvers equipped with XOR-reasoning techniques on random CNF-XOR formulas. 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. On the theoretical front, we prove that the solution space of a random CNF-XOR formula 'shatters' at all nonzero XOR-clause densities into well-separated components, similar to the behavior seen in random CNF formulas known to be difficult for many SAT algorithms.
    Combining the k-CNF and XOR Phase-Transitions
    Jeffrey M. Dudek, Kuldeep S. Meel, and Moshe Y. Vardi
    Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2016.
    The runtime performance of modern SAT 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 SAT 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.