Vijay K. Garg

Robert P. Streit, Vijay K. Garg

A greedoid is a generalization of a matroid allowing for more flexible analyses and modeling of combinatorial optimization problems. However, these structures decimate many matroid properties contributing to their pervasive nature. A polymatroid greedoid [KL85] presents an interesting middle ground, so we further develop this class. First we prove every local poset greedoid for which the greedy algorithm correctly solves linear optimizations over its basic words must have a polymatroid representation. For this, we use relationships between the lattices of greedoid flats and closed sets of a polymatroid to generalize concepts in [KL85]. Then, we show our generalization is defined by a Galois connection between the greedoid flats and closed sets of a representation. Finally, we apply this duality to identify a subclass of polymatroid greedoids with favorable properties, which we call strong polymatroid greedoids. As technical tools for our analyses, we introduce optimism and the Forking Lemma for interval greedoids. Both are pervasive in our work, and are of independent interest.

Abdullah H. Rasheed, Vijay K. Garg

Many modern solvers and program analyzers rely on non-monotone reasoning (e.g. negation-as-failure, speculative updates, backtracking) for which classical monotone fixed-point methods do not apply. The general problem of finding the fixed points of these processes is a difficult one. For this reason, there have been theoretical efforts in existing Approximation Fixpoint Theory (AFT) from the domain of logic programming to approximate fixed points of non-monotone operators. Tight approximations of these fixed points are highly useful for accelerating non-monotonic computations by restricting the search space. In practice, however, even the best approximations obtained through AFT can be coarse and computationally expensive. We aim to address both issues to make AFT approximation methods practical for use in programming languages (PL) settings. To mitigate inefficiency, we prove the soundness of an abstract interpretation for approximating operators. To improve upon coarse approximations, we carefully introduce controlled unsoundness to design an effective yet practical algorithm for partitioning and tightening AFT's best approximations. This algorithm is sound, anytime, and guarantees termination on finite-height lattices. We further present a modification that ensures polynomial-time complexity. We instantiate these methods in two settings: (1) answer set programming, where it serves as a convergence-accelerating pre-processor, and (2) speculative program analysis, where it reduces rollback while preserving soundness. In both settings, we focus on implementation-level details to demonstrate the practical applicability of our methods.

David Ribeiro Alves, Vijay K. Garg

Traditional lock-free parallel algorithms for combinatorial optimization problems, such as shortest paths, stable matching, and job scheduling require programmers to write problem-specific routines and synchronization code. We propose a general-purpose lock-free runtime, LLP-FW that can solve all combinatorial optimization problems that can be formulated as a Lattice-Linear Predicate by advancing all forbidden local states in parallel until a solution emerges. The only problem-specific code is a definition of the forbiddenness check and a definition of the advancement. We show that LLP-FW can solve several different combinatorial optimization problems, such as Single Source Shortest Paths (SSSP), Breadth-First Search (BFS), Stable Marriage, Job Scheduling, Transitive Closure, Parallel Reduction, and 0-1 Knapsack. We compare LLP-FW against hand-tuned, custom solutions for these seven problems and show that it compares favorably in the majority of cases.