| Total: 27
Model counting of Disjunctive Normal Form (DNF) formulas is a critical problem in applications such as probabilistic inference and network reliability. For example, it is often used for query evaluation in probabilistic databases. Due to the computational intractability of exact DNF counting, there has been a line of research into a variety of approximation algorithms. We develop a new Monte Carlo approach with an adaptive stopping rule and short-circuit formula evaluation. We prove it achieves Probably Approximately Correct (PAC) learning bounds and has asymptotically improved time and randomness complexity compared to previous methods. We also show experimentally that it out-performs prior algorithms by at least three orders of magnitude in running time and scalability.
Optimization problems such as Viterbi decoding and V-optimal histogram construction seek a path of exact length L through a state space that minimizes a cost function. These problems are traditionally solved using dynamic programming (DP). A best-first-search (BFS) solution is also applicable, yet requires maintaining a priority queue. In all cases, memory usage grows linearly with both state space size and path length. In this paper, we propose CompactBFS, a framework that limits the growth of the BFS priority queue to space-efficiently determine the exact optimal cost for a fixed-length path and then constructs such a path by a divide-and-conquer strategy that eliminates the memory overhead. We apply CompactBFS to Viterbi decoding, which remains relevant to speech recognition, and V-optimal histogram construction. Our experimental results demonstrate significant gains over state-of-the-art solutions in runtime and memory consumption.
Joint optimization of pricing, dispatching, and routing is critical for hub-based mobility services but challenging due to complex decision couplings and strict service guarantees, such as Order Response Rate (ORR). Conventional constrained reinforcement learning often struggles in this mixed continuous--combinatorial action space, suffering from oscillatory behavior in Lagrangian dual variables and unstable constraint satisfaction. To address this, we propose PID-SACA, a unified framework that integrates an entropy-regularized actor--critic policy for continuous pricing and dispatching assisted by an embedded routing solver for execution-aware feedback. Crucially, we adapt the PID control mechanism to the Lagrangian dual update process. This approach leverages proportional, integral, and derivative feedback to dampen oscillations caused by stochastic gradient variance, ensuring robust long-term constraint enforcement. We provide theoretical analysis on the boundedness of dual variables, and experiments on publicly available large-scale mobility datasets demonstrate that PID-SACA significantly outperforms baselines, achieving high revenue with stable service compliance. Code: https://github.com/jerry0375/PID-SACA
Decision-focused learning has shown great promise for addressing predict-then-optimize problems, particularly in the presence of under-specified models. However, its practical deployment is often hindered by high computational costs and limited scalability, as it requires solving a constrained optimization problem for each training instance at every iteration. To address these challenges, we propose a novel framework that incorporates Lagrangian decomposition into the decision-focused learning paradigm. Specifically, we introduce a new surrogate objective along with two loss functions for evaluating and training the underlying prediction model. We further propose two variants of our approach, which offer different trade-offs between computational efficiency and solution quality. Our framework can be seamlessly integrated with standard decision-focused learning methods, including Smart Predict-then-Optimize (SPO+) and Implicit Maximum Likelihood Estimation (IMLE). Through experiments on two standard benchmarks, the multi-dimensional knapsack problem and quadratic portfolio optimization, we demonstrate that our approach achieves competitive performance while remaining amenable to parallelization. In particular, it consistently outperforms traditional decision-focused learning methods on large-scale instances, involving up to eight times more variables than those typically considered in related work. The implementation is available at https://github.com/corail-research/DFL-LD.
The Simple Temporal Problem (STP) is a core framework for quantitative temporal constraints. As STP data can be inconsistent, we study MaxSTP: compute a maximum-cardinality consistent subset of constraints. This extension is NP-hard, and we analyze its parameterized complexity under measures that capture practically relevant instance features: the number of variables n (instance scale), the maximum coefficient magnitude k (numeric range), and structural parameters of the constraint graph such as treewidth tw (decomposability), and vertex cover size vc (density). We show that MaxSTP is W[1]-hard parameterized by n, implying that n and parameters that depend on n (including tw and vc) are insufficient for fixed-parameter tractability. For combined parameters, we give an O^*(k^n)-time algorithm, yielding single-exponential solvability for fixed k. While k+tw remains W[1]-hard, MaxSTP is in XP via an O^*((n * k)^tw) algorithm. Our results suggest that MaxSTP is often computationally harder than optimizing qualitative CSPs - we verify that many such problems (including RCC-8 and Allen's algebra) are FPT when parameterized by n or tw. However, we also demonstrate that FPT algorithms for MaxSTP are indeed possible but with other parameters such as k + vc.
Factored tasks are a classical planning representation that extends SAS+ with limited forms of disjunctive preconditions, conditional effects, and angelic nondeterminism. This added expressiveness allows for a more compact representation of taks than traditional formalisms such as STRIPS or SAS+, and supports a wide range of task transformations. However, existing planning approaches for factored tasks have been limited to heuristic search methods. In this work, we investigate how to encode factored tasks in SAT. We propose several ways to encode the tasks, focusing on different strategies for translating the factored transition relation into propositional logic. We also analyze how to exploit parallelism at various levels in this setting and study the impact of common task transformations on the performance of SAT-based planners.
We introduce QUINTIC, a general algorithm for actively learning quantitative automata from preferences. Quantitative automata evaluate input sequences by applying a valuation function---such as sum, product, or average---to the output labels of the states visited. Such models naturally arise in use cases ranging from probabilistic verification, sequence classification, and sequential decision making. However, existing learning approaches, such as variants of L*, weighted‐automata learning algorithms, and active learning preference‐driven methods, either assume finite output alphabets or restrict the valuation function to particular forms. QUINTIC utilizes a symbolic observation table and applies deductive reasoning with the assistance of an SMT solver to identify the correct minimal state, transition, and state label combination of the quantitative automaton. The deductive reasoning relies on the minimal combination of theories determined by the valuation function and output alphabet. Consequently, QUINTIC has completeness, minimalism, and query complexity guarantees, and learns quantitative automata across finite, integer, and rational outputs. Our extensive experiments show how QUINTIC scales under weak or strong feedback, and alternative MaxSMT objectives.
Satisfiability (SAT) with cardinality constraints arises naturally in many practical applications, where high-level counting requirements coexist with standard Conjunctive Normal Form (CNF) clauses. Translating these constraints into CNF can destroy structural information, limiting the effectiveness of search-based heuristics. In this paper, we propose a cardinality-aware local search framework to solve this problem, denoted as CardSAT-LS. CardSAT-LS integrates a preprocessing phase based on the generalized unit propagation and resolution, a cardinality-sensitive scoring function combining the make-break mechanism and cardinality violation, and an initialization based on fake-backbone variables. Furthermore, CardSAT-LS employs a unified framework that adaptively alternates between flip and swap operators when the search gets trapped in local optima. Finally, we conduct experiments on five public benchmarks from real-world applications as well as the MaxSAT and SAT competitions. Compared with ten state-of-the-art competitors, including SAT, MaxSAT, and PB solvers, CardSAT-LS solves the most instances with the lowest PAR-2 score. Additionally, we integrate CardSAT-LS into exact solvers for phase selection, which leads to significant speedups.
The Maximum Weight Clique Problem (MWCP) is NP-hard and is typically solved exactly within a Branch-and-Bound (BnB) framework, where the quality of upper bounds critically determines the pruning efficiency. Recent solvers enhance independent-set-based bounds using MaxSAT reasoning. However, their effectiveness is limited by two inherent limitations: (i) independent sets in conflicts are discarded after a single use, preventing their reuse in subsequent reasoning; and (ii) conflicts are detected in a fixed order regardless of their potential contribution to bound tightening. To address these issues, we propose two complementary techniques. The UnLocking Mechanism (ULM) preserves conflict cores and enables the reuse of independent sets in subsequent reasoning, while the Benefit-Enhanced Strategy (BES) steers the MaxSAT reasoning process toward conflicts and independent sets with higher pruning potential. By integrating ULM and BES, we develop a new solver, ULE-MWC (UnLocking Enhanced MWC). Experimental results on standard benchmarks show that ULE-MWC consistently yields tighter upper bounds and outperforms state-of-the-art exact solvers in both runtime and search efficiency.
Optimizing survival outcomes, such as patient survival or customer retention, is a critical objective in data-driven decision-making. Off-Policy Evaluation (OPE) provides a powerful framework for assessing such decision-making policies using logged data alone, without the need for costly or risky online experiments in high-stakes applications. However, typical estimators are not designed to handle right-censored survival outcomes, as they ignore unobserved survival times beyond the censoring time, leading to systematic underestimation of the true policy performance. To address this issue, we propose a novel framework for OPE and Off-Policy Learning (OPL) tailored for survival outcomes under censoring. Specifically, we introduce IPCW-IPS and IPCW-DR, which employ the Inverse Probability of Censoring Weighting technique to explicitly deal with censoring bias. We theoretically establish that our estimators are unbiased and that IPCW-DR achieves double robustness, ensuring consistency if either the propensity score or the outcome model is correct. Furthermore, we extend this framework to constrained OPL to optimize policy value under budget constraints. We demonstrate the effectiveness of our proposed methods through simulation studies and illustrate their practical impacts using public real-world data for both evaluation and learning tasks.
We present complementary branching, a new branching approach for model counting based on the complement counting paradigm. Instead of branching on individual variables, complementary branching decomposes the counting problem for arbitrary CNF formulas into several subformulas, which naturally augments the classic DPLL branching. We show two novel results in which the main tool is complementary branching. First, we design new #SAT algorithms for sparse CNF formulas running in time O*(2^(alpha n)), for some constant alpha < 1. As a second application, we improve the best known deterministic upper bound for #3-SAT to O*(1.637^n) by using a version of clause learning based on complementary branching. These results demonstrate that complementary branching is a powerful tool for designing faster exact algorithms for propositional model counting.
Hybrid tables, also referred to as `smart' in the literature, represent a valuable modeling technique within Constraint Programming (CP). These tables allow us to handle disjunctive cases (constraining expressions) in a compact and structured way, by authorizing tuples (table entries) to contain simple unary and binary arithmetic restrictions (similar to internal constraints). In this paper, we show the practical interest of using hybrid tables for planning-like combinatorial puzzles, when the transition from one state to the next can be encoded by a single hybrid table. Experimental results show that these hybrid models exhibit greater compactness and efficiency in solving compared to their conventional counterparts.
Given a social network ? with n nodes and m edges, the opinion maximization (OM) problem aims at identifying k (k ≪ n) opinion leaders to maximize their opinion propagation in ?. Despite its significance and prevalence, existing OM methods often struggle to strike a satisfactory balance between theoretical performance and practical efficiency. This paper provides an inverse optimization perspective for OM by reformulating it as an opinion minimization (OMin) problem, whose objective function holds succinct expression and desired properties. Then, we introduce a bounded estimation scheme (BES) that can estimate the objective function of OMin with bounded error in Õ(kn+m) expected time, thereby making the optimization for OMin more efficient. To further enhance the optimization efficiency, a decomposition-based decremental estimation algorithm (DDEA) with a near (1-1/e) approximation ratio in Õ(kmn) expected time is specifically designed for OMin. Extensive experiments on real-world social networks of varying scales demonstrate the effectiveness of BES and the superiority of DDEA.
Despite decades of intensive research and optimization, modern Boolean Satisfiability (SAT) solvers have reached a plateau where significant performance gains are increasingly difficult to achieve. While Large Language Models (LLMs) have demonstrated remarkable capabilities in pattern recognition and code generation for combinatorial optimization, their direct application to highly optimized SAT solvers remains a formidable challenge due to the extreme complexity and sensitivity of solver heuristics. In this paper, we introduce AESAT (Auto-Evolving SAT solving), a novel neuro-symbolic framework designed to automatically evolve and optimize the heuristic functions of SAT solvers. AESAT employs a memetic-inspired approach, synergizing LLM-guided individual optimization with evolutionary exploration. By leveraging self-optimized prompting techniques, our framework enables LLMs to iteratively discover and refine sophisticated heuristics that bypass the limitations of human-engineered designs. The efficacy of AESAT is demonstrated by its flagship derivative, AE-Kissat-MAB, which won the main track of the 2025 International SAT Competition by a wide margin. This result represents the first time an LLM-enhanced solver has dominated the world's premier SAT competition, marking a paradigm shift in the automated design of reasoning algorithms.
Spectral relaxation is widely used for large-scale combinatorial optimization due to its computational efficiency. Yet its effectiveness depends critically on the choice of graph normalization, a design decision typically made heuristically. Here, we show that normalization can be treated as a continuous optimization variable rather than a fixed preprocessing choice. Our method, Differentiable Spectral Normalization (DSN), parameterizes the spectral relaxation through a diagonal metric and maximizes the resulting lower bound via projected gradient ascent. Exact gradients are obtained through the Hellmann-Feynman theorem using only the principal eigenpair, maintaining linear complexity per iteration. On benchmark instances ranging from 10^3 to 8.4 x 10^6 nodes, DSN improves solution quality by 3-15% over static spectral methods. Its performance comes within 1-3% of state-of-the-art metaheuristics, such as simulated annealing, at up to 190x lower computational cost on large-scale instances. These results suggest that learning problem-specific relaxation geometry can substantially close the gap between spectral scalability and metaheuristic solution quality.
In this work, we propose the first constant-approximation algorithms, LinAst and LinAtg, which simultaneously achieve optimal query complexity O(n) and adaptive complexity O(log n) for non-monotone submodular maximization under a cardinality constraint k over a ground set of size n. Specifically, compared with existing algorithms that attain the best known adaptive complexity of O(log n), our approach preserves this adaptivity while reducing the query complexity from O(n log k) to O(n) and improving the approximation ratio from 0.172-epsilon to 0.193-epsilon. Our algorithms are built upon LinAdapt, which achieves a constant approximation ratio with O(log n) adaptive rounds and linear query complexity by requiring only O(1) candidate guesses of the optimal value. We further introduce the BoostAdapt algorithm, which improves the approximation guarantee to 0.25-\epsilon with O(log n log k) adaptive complexity and O(n log k) query complexity, based on a novel staggered greedy threshold framework that alternately constructs two disjoint solution sets over O(log k) sequential rounds. Extensive experiments on standard benchmark datasets demonstrate that our algorithms consistently outperform state-of-the-art methods in terms of solution quality, query complexity, and running time.
When solving optimization problems under uncertainty with contextual data, utilizing machine learning to predict the uncertain parameters' values is a popular and effective approach. Decision-focused learning (DFL) aims at learning a predictive model such that decision quality, instead of prediction accuracy, is maximized. Common practice is to predict a single scenario representing the uncertain parameters, implicitly assuming that there exists a deterministic problem approximation (proxy) that allows for optimal decision-making. The opposite has also been considered, where the underlying distribution is estimated with a parameterized distribution. However, little is known about when either choice is valid. This paper investigates for the first time problem properties that justify using a certain decision proxy. Using this, we present alternative decision proxies for DFL, with little or no compromise on the complexity of the learning task. We show the effectiveness of presented approaches in experiments on continuous and discrete problems, as well as problems with uncertainty in the objective function and in the constraints.
Join ordering is the NP-hard problem of selecting the most efficient order in which to evaluate joins (conjunctive, binary operators) in a database query. Because query execution performance critically depends on this choice, join ordering lies at the core of query optimization. Traditional approaches cast this problem as a discrete combinatorial search over binary trees guided by a cost model, but they have trade-offs between effectiveness and efficiency. We show that when the cost model is differentiable, query plans can be continuously relaxed into a soft adjacency matrix that represents a superposition of plans. This continuous relaxation, combined with differentiable constraints that enforce plan validity, enables a gradient-based search for low-cost plans within this relaxed space. Using a Graph Neural Network as the cost model, we demonstrate that this gradient-based approach can find comparable and even lower-cost plans compared to traditional discrete search methods on two different graph datasets. Furthermore, we empirically show that the runtime of this approach scales better than discrete search algorithms. We believe this first step towards gradient-based join ordering can lead to more effective and efficient query optimizers in the future.
The Kidney Exchange Problem is a prominent challenge in healthcare and economics, arising in the context of organ transplantation. It has been extensively studied in artificial intelligence and optimization. In a kidney exchange, a set of donor-recipient pairs and altruistic donors are considered, with the goal of identifying a sequence of exchanges—comprising cycles or chains starting from altruistic donors—such that each donor provides a kidney to the compatible recipient in the next donor-recipient pair. These exchanges create a network of transplants aimed at maximizing the total number, t, of successful transplants. Due to constraints in medical resources, limits are often imposed on the lengths of these cycles and chains. Recently, this problem was deterministically solved in O* (14.34ᵗ) time (IJCAI 2024). In this paper, we introduce the representative set technique for the Kidney Exchange Problem, showing that the problem can be deterministically solved in O* (6.855ᵗ) time.
Fairness k-submodular maximization has attracted increasing interest due to its broad relevance in artificial intelligence and machine learning. However, most existing works are limited to monotone objectives or simple size constraints, while non-monotone settings with richer constraints remain largely unexplored. In this paper, we first introduce a constant-factor approximation algorithm for the problem with a general non-monotone objective function under a matroid constraint. Our approach is built upon a two-stage algorithmic framework. Specifically, we first develop an algorithm that guarantees feasibility with respect to upper fairness bounds only. We then show how this algorithm can be systematically extended to simultaneously enforce fairness bounds, while preserving provable approximation guarantees. Comprehensive experiments on standard benchmark datasets demonstrate that our algorithm achieves competitive objective values while maintaining a favorable balance between fairness guarantees and query complexity efficiency compared to existing state-of-the-art methods.
Post-training quantization (PTQ) is widely used to compress large language models without retraining. However, many existing weight-only methods rely on heuristic objectives and greedy rounding strategies, leading to noticeable degradation under low-bit quantization. We propose OJBKQ, a layer-wise PTQ method that formulates weight quantization as a joint optimization problem over activations and weights, yielding a multiple-right-hand-side box-constrained integer least squares (BILS) problem per layer. To solve this NP-hard problem, we extend Klein’s randomized variant of Babai’s nearest-plane algorithm to handle box constraints and run the extended algorithm K times to generate K box-constrained Klein points. The minimum-residual candidate among these points and the box-constrained Babai point is selected as a suboptimal solution. Experiments on large language models show that OJBKQ achieves lower perplexity at 3–4 bits than existing PTQ methods, while maintaining comparable computational cost.
Model editing updates a pre-trained LLM with new facts or rules without retraining while preserving unrelated behavior. In real deployment, edits arrive as long streams, creating a plasticity–stability dilemma: repeated locate-then-edit “hard writes” can accumulate interference over time, while rigid preservation constraints may protect only explicitly constrained directions, allowing past edits or unconstrained behaviors to deviate. We propose RLSEdit, a recursive least-squares editor for long sequential editing. RLSEdit formulates editing as an online quadratic optimization with soft constraints, minimizing a cumulative key-value fitting objective together with two regularizers that control deviation from the pre-trained weights and from a designated anchor mapping. This objective admits an efficient Woodbury-based online recursion, with per-edit cost independent of history length and scaling only with the current edit size. We further provide deviation bounds and an asymptotic characterization of the adherence–preservation trade-off in the many-edits regime. Experiments on CounterFact and ZsRE across multiple model families show stable scaling to 10K edits, outperforming strong baselines in both edit success and holistic stability, while retaining early edits and preserving general capabilities on GLUE and held-out reasoning/code benchmarks. Code will be at here.
Singleton consistency significantly reduces the search space of backtracking search for solving constraint satisfaction problems (CSP). However, it is too expensive to be used throughout the search, and it has not been successfully applied in solving general CSPs. In this paper, we propose a variable-oriented adaptive singleton consistency, namely VOASC, that could be applied in general-purpose constraint solvers. It calculates the filtering efficiency of local consistency enforced by the default propagation engine and the singleton-based consistency for each variable, and then selects an appropriate consistency to propagate the decisions of the variable in subsequent searches. We performed extensive experimentation with the MiniZinc benchmark suite. VOASC demonstrates superior solving performance on both CSP and COP, compared to the two candidate local consistencies and several existing adaptive propagation methods.
Structured output generation is increasingly critical for real-world AI systems, particularly in on-device settings where small language models (0.5B–8B parameters) must produce machine-executable outputs under strict latency and privacy constraints. Although constrained decoding provides formal guarantees of structural validity without retraining, its effectiveness across different tasks, models, and constraint formalisms remains insufficiently understood. We introduce StructureBench, a comprehensive benchmark for structured generation on edge devices, covering JSON and tool-call generation, code synthesis, mathematics, science, and domain-specific languages, and evaluating over 11 on-device language and vision–language models spanning 0.5B–8B parameters. StructureBench systematically compares prompt-based generation with three widely used constrained decoding frameworks—Outlines, XGrammar, and Guidance—and adopts decoupled metrics to separately assess structural validity and semantic correctness. Our experiments show that constrained decoding consistently enforces syntactic validity, but does not reliably improve semantic accuracy and may even degrade performance for smaller models or complex grammars. These findings reveal clear task- and model-dependent boundaries for effective constrained decoding and highlight the need for scenario-aware adaptation in on-device structured generation. We release StructureBench at https://github.com/Str-Ben/StructureBench.
Propositional Model Counting (#SAT) is essential for probabilistic reasoning but faces scalability limits on single cores. Existing distributed approaches struggle with high initialization overheads (static decomposition) or rigid architecture. We propose a novel, generic framework for distributed exact model counting. Leveraging C++ templates, our architecture decouples parallel orchestration from solving logic, enabling state-of-the-art solvers to be parallelized with minimal modification. We implement an adaptive work-stealing strategy that ensures effective load balancing. Experiments on competition benchmarks show that our approach achieves near-linear scalability and significantly outperforms existing distributed solvers.