Jeffrey Dudek

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:
  • Tensor Networks
  • 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

    ADDMC: Weighted Model Counting with Algebraic Decision Diagrams
    Jeffrey M. Dudek, Vu H.N. Phan, and Moshe Y. Vardi
    Proceedings of Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI), 2020.
    We present an algorithm to compute exact literal-weighted 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 state-of-the-art 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
    Jeffrey M. Dudek, Dror Fried
    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 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.