Jeffrey Dudek

I am a 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

    ProCount: Weighted Projected Model Counting with Graded Project-Join Trees
    Jeffrey M. Dudek, Vu H.N. Phan, and Moshe Y. Vardi
    Proceedings of International Conference on Theory and Applications of Satisfiability Testing (SAT), 2021.
    Recent work in weighted model counting proposed a unifying framework for dynamic-programming algorithms. The core of this framework is a project-join tree: an execution plan that specifies how Boolean variables are eliminated. We adapt this framework to compute exact literal-weighted projected model counts of propositional formulas in conjunctive normal form. Our key conceptual contribution is to define gradedness on project-join trees, a novel condition requiring irrelevant variables to be eliminated before relevant variables. We prove that building graded project-join trees can be reduced to building standard project-join trees and that graded project-join trees can be used to compute projected model counts. The resulting tool ProCount is competitive with the state-of-the-art tools D4P, projMC, and reSSAT, achieving the shortest solving time on 131 benchmarks of 390 benchmarks solved by at least one tool, from 849 benchmarks in total.
    Taming Discrete Integration via the Boon of Dimensionality
    Jeffrey M. Dudek, Dror Fried, and Kuldeep S. Meel
    Proceedings of Neural Information Processing Systems (NeurIPS), 2020.
    Discrete integration is a fundamental problem in computer science that concerns the computation of discrete sums over exponentially large sets. Despite intense interest from researchers for over three decades, the design of scalable techniques for computing estimates with rigorous guarantees for discrete integration remains the holy grail. The key contribution of this work addresses this scalability challenge via an efficient reduction of discrete integration to model counting. The proposed reduction is achieved via a significant increase in the dimensionality that, contrary to conventional wisdom, leads to solving an instance of the relatively simpler problem of model counting.
    Building on the promising approach proposed by Chakraborty et al, our work overcomes the key weakness of their approach: a restriction to dyadic weights. We augment our proposed reduction, called DeWeight, with a state of the art efficient approximate model counter and perform detailed empirical analysis over benchmarks arising from neural network verification domains, an emerging application area of critical importance. DeWeight, to the best of our knowledge, is the first technique to compute estimates with provable guarantees for this class of benchmarks.
    DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees
    Jeffrey M. Dudek, Vu H.N. Phan, and Moshe Y. Vardi
    Proceedings of International Conference on Principles and Practice of Constraint Programming (CP), 2020.
    We propose a unifying dynamic-programming framework to compute exact literal-weighted model counts of formulas in conjunctive normal form. At the center of our framework are project-join trees, which specify efficient project-join orders to apply additive projections (variable eliminations) and joins (clause multiplications). In this framework, model counting is performed in two phases. First, the planning phase constructs a project-join tree from a formula. Second, the execution phase computes the model count of the formula, employing dynamic programming as guided by the project-join tree. We empirically evaluate various methods for the planning phase and compare constraint-satisfaction heuristics with tree-decomposition tools. We also investigate the performance of different data structures for the execution phase and compare algebraic decision diagrams with tensors. We show that our dynamic-programming model-counting framework DPMC is competitive with the state-of-the-art exact weighted model counters cachet, c2d, d4, and miniC2D.
    Parallel Weighted Model Counting with Tensor Networks
    Jeffrey M. Dudek, Moshe Y. Vardi
    Proceedings of SAT Workshop on Model Counting (MCW), 2020.
    A promising new algebraic approach to weighted model counting makes use of tensor networks, following a reduction from weighted model counting to tensor-network contraction. Prior work has focused on analyzing the single-core performance of this approach, and demonstrated that it is an effective addition to the current portfolio of weighted-model-counting algorithms.
    In this work, we explore the impact of multi-core and GPU use on tensor-network contraction for weighted model counting. To leverage multiple cores, we implement a parallel portfolio of tree-decomposition solvers to find an order to contract tensors. To leverage a GPU, we use TensorFlow to perform the contractions. We compare the resulting weighted model counter on 1914 standard weighted model counting benchmarks and show that it significantly improves the virtual best solver.
    ADDMC: Weighted Model Counting with Algebraic Decision Diagrams
    Jeffrey M. Dudek, Vu H.N. Phan, and Moshe Y. Vardi
    Proceedings of 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.
    Efficient Contraction of Large Tensor Networks for Weighted Model Counting through Graph Decompositions
    Jeffrey M. Dudek, Leonardo DueƱas-Osorio, Moshe Y. Vardi
    (Preprint) Submitted to Artificial Intelligence Journal, 2019.
    Constrained counting is a fundamental problem in artificial intelligence. A promising new algebraic approach to constrained counting makes use of tensor networks, following a reduction from constrained counting to the problem of tensor-network contraction. Contracting a tensor network efficiently requires determining an efficient order to contract the tensors inside the network, which is itself a difficult problem.
    In this work, we apply graph decompositions to find contraction orders for tensor networks. We prove that finding an efficient contraction order for a tensor network is equivalent to the well-known problem of finding an optimal carving decomposition. Thus memory-optimal contraction orders for planar tensor networks can be found in cubic time. We show that tree decompositions can be used both to find carving decompositions and to factor tensor networks with high-rank, structured tensors.
    We implement these algorithms on top of state-of-the-art solvers for tree decompositions and show empirically that the resulting weighted model counter is quite effective and useful as part of a portfolio of counters.
    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.
    The names of authors are sorted alphabetically and the order does not reflect contribution.