GenAI4ELab/papercli-papers huggingface dataset:
Complete Symmetry Breaking for Finite Models
Authors: Marek Dančo; Mikoláš Janota; Michael Codish; João Jorge Araújo
Venue: AAAI 2025 (main)

Abstract: This paper introduces a SAT-based technique that calculates a compact and complete symmetry-break for finite model finding, with the focus on structures with a single binary operation (magmas). Classes of algebraic structures are typically described as first-order logic formulas and the concrete algebras are models of these formulas.  Such models include an enormous number of isomorphic, i.e. symmetric, algebras.

A complete symmetry-break is a formula that has as models, exactly one canonical representative from each equivalence class of algebras. Thus, we enable answering questions about properties of the models so that computation and search are restricted to the set of canonical representations.

For instance, we can answer the question: How many non-isomorphic semigroups are there of size n?  Such questions can be answered by counting the satisfying assignments of a SAT formula, which already filters out non-isomorphic models. The introduced technique enables us calculating numbers of algebraic structures not present in the literature and going beyond the possibilities of pure enumeration approaches.
Decentralized Projected Riemannian Stochastic Recursive Momentum Method for Nonconvex Optimization
Authors: Kangkang Deng; Jiang Hu
Venue: AAAI 2025 (main)

Abstract: This paper studies decentralized optimization over a compact submanifold within a communication network of n nodes, where each node possesses a smooth non-convex local cost function, and the goal is to jointly minimize the sum of these local costs. We focus particularly on the online setting, where local data is processed in real-time as it streams in, without the need for full data storage. We propose a decentralized projected Riemannian stochastic recursive momentum (DPRSRM) method that employs local hybrid stochastic gradient estimators and uses the network to track the global gradient. DPRSRM achieves an oracle complexity of  O(epsilon^(-3/2)), outperforming existing methods that have at most O(epsilon^(-2)) complexity. Our method requires only O(1) gradient evaluations per iteration for each local node and does not require restarting with a large batch gradient.   Furthermore, we demonstrate the effectiveness of our proposed methods compared to state-of-the-art ones through numerical experiments on principal component analysis problems and low-rank matrix completion.
SORREL: Suboptimal-Demonstration-Guided Reinforcement Learning for Learning to Branch
Authors: Shengyu Feng; Yiming Yang
Venue: AAAI 2025 (main)

Abstract: Mixed Integer Linear Program (MILP) solvers are mostly built upon a Branch-and-Bound (B&B) algorithm, where the efficiency of traditional solvers heavily depends on hand-crafted heuristics for branching. The past few years have witnessed the increasing popularity of data-driven approaches to automatically learn these heuristics. However, the success of these methods is highly dependent on the availability of high-quality demonstrations,  which requires either the development of near-optimal heuristics or a time-consuming sampling process. This paper averts this challenge by proposing Suboptimal-Demonstration-Guided Reinforcement Learning (SORREL) for learning to branch. SORREL selectively learns from suboptimal demonstrations based on value estimation. It utilizes suboptimal demonstrations through both offline reinforcement learning on the demonstrations generated by suboptimal heuristics and self-imitation learning on past good experiences sampled by itself. Our experiments demonstrate its advanced performance in both branching quality and training efficiency over previous methods for various MILPs.
Langevin Multiplicative Weights Update with Applications in Polynomial Portfolio Management
Authors: Yi Feng; Xiao Wang; Tian Xie
Venue: AAAI 2025 (main)

Abstract: We consider nonconvex optimization problem over simplex, and more generally, a product of simplices. We provide an algorithm, Langevin Multiplicative Weights Update (LMWU) for solving global optimization problems by adding a noise scaling with the non-Euclidean geometry in the simplex. Non-convex optimization has been extensively studied by machine learning community due to its application in various scenarios such as neural network approximation and finding Nash equilibrium. Despite recent progresses on provable guarantee of escaping and avoiding saddle point (convergence to local minima) and global convergence of Langevin gradient based method without constraints, the global optimization with constraints is less studied. We show that LMWU algorithm is provably convergent to interior global minima with a non-asymptotic convergence analysis. We verify the efficiency of the proposed algorithm in real data set from polynomial portfolio management, where optimization of a highly non-linear objective function plays a crucial role.
Parameterized Complexity of Caching in Networks
Authors: Robert Ganian; Fionn Mc Inerney; Dimitra Tsigkari
Venue: AAAI 2025 (main)

Abstract: The fundamental caching problem in networks asks to find an allocation of contents to a network of caches with the aim of maximizing the cache hit rate. Despite the problem's importance to a variety of research areas - including not only content delivery, but also edge intelligence and inference - and the extensive body of work on empirical aspects of caching, very little is known about the exact boundaries of tractability for the problem beyond its general NP-hardness. We close this gap by performing a comprehensive complexity-theoretic analysis of the problem through the lens of the parameterized complexity paradigm, which is designed to provide more precise statements regarding algorithmic tractability than classical complexity. Our results include algorithmic lower and upper bounds which together establish the conditions under which the caching problem becomes tractable.
FFCG: Effective and Fast Family Column Generation for Solving Large-Scale Linear Program
Authors: Yi-Xiang Hu; Feng Wu; Shaoang Li; Yifang Zhao; Xiang-Yang Li
Venue: AAAI 2025 (main)

Abstract: Column Generation (CG) is an effective and iterative algorithm to solve large-scale linear programs (LP). During each CG iteration, new columns are added to improve the solution of the LP. Typically, CG greedily selects one column with the most negative reduced cost, which can be improved by adding more columns at once. However, selecting all columns with negative reduced costs would lead to the addition of redundant columns that do not improve the objective value. Therefore, selecting the appropriate columns to add is still an open problem and previous machine-learning-based approaches for CG only add a constant quantity of columns per iteration due to the state-space explosion problem. To address this, we propose Fast Family Column Generation (FFCG) — a novel reinforcement-learning-based CG that selects a variable number of columns as needed in an iteration. Specifically, we formulate the column selection problem in CG as an MDP and design a reward metric that balances both the convergence speed and the number of redundant columns. In our experiments, FFCG converges faster on the common benchmarks and reduces the number of CG iterations by 77.1% for Cutting Stock Problem (CSP) and 84.8% for Vehicle Routing Problem with Time Windows (VRPTW), and a 71.4% reduction in computing time for CSP and 84.0% for VRPTW on average compared to several state-of-the-art baselines.
Breaking Symmetries in Quantified Graph Search: A Comparative Study
Authors: Mikoláš Janota; Markus Kirchweger; Tomáš Peitl; Stefan Szeider
Venue: AAAI 2025 (main)

Abstract: Graph generation and enumeration problems often require handling equivalent graphs---those that differ only in vertex labeling. We study how to extend SAT Modulo Symmetries (SMS), a framework for eliminating such redundant graphs, to handle more complex constraints. While SMS was originally designed for constraints in propositional logic (in NP), we now extend it to handle quantified Boolean formulas (QBF), allowing for more expressive specifications like non-3-colorability (a coNP-complete property). We develop two approaches: a static QBF encoding and a dynamic method integrating SMS into QBF solvers. Our analysis reveals that while specialized approaches can be faster, QBF-based methods offer easier implementation and formal verification capabilities.
A Complete Algorithm for Optimization Modulo Nonlinear Real Arithmetic
Authors: Fuqi Jia; Yuhang Dong; Rui Han; Pei Huang; Minghao Liu; Feifei Ma; Jian Zhang
Venue: AAAI 2025 (main)

Abstract: Optimization Modulo Nonlinear Real Arithmetic, abbreviated as OMT(NRA), generally focuses on optimizing a given objective subject to quantifier-free Boolean combinations of primitive constraints, including Boolean variables, polynomial equations, and inequalities. It is widely applicable in areas like program verification, analysis, planning, and so on. The existing solver, OptiMathSAT, officially supporting OMT(NRA), employs an incomplete algorithm. We present a sound and complete algorithm, Optimization Cylindrical Algebraic Covering (OCAC), integrated within the Conflict-Driven Clause Learning (CDCL) framework, specifically tailored for OMT(NRA) problems. We establish the correctness and termination of CDCL(OCAC) and explore alternative approaches using cylindrical algebraic decomposition (CAD) and first-order formulations. Our work includes the development of the first complete OMT solver for NRA, demonstrating significant performance improvements. In benchmarks generated from SMT-LIB instances, our algorithm finds the optimum value in about 150% more instances compared to the current leading solver, OptiMathSAT.
DCC: Differentiable Cardinality Constraints for Partial Index Tracking
Authors: Wooyeon Jo; Hyunsouk Cho
Venue: AAAI 2025 (main)

Abstract: Index tracking is a popular passive investment strategy aimed at optimizing portfolios, but fully replicating an index can lead to high transaction costs. To address this, partial replication have been proposed. However, the cardinality constraint renders the problem non-convex, non-differentiable, and often NP-hard, leading to the use of heuristic or neural network-based methods, which can be non-interpretable or have NP-hard complexity. To overcome these limitations, We propose a Differentiable Cardinality Constraint (DCC) for index tracking and introduce a floating-point precision-aware method to address implementation issues. We theoretically prove our methods calculate cardinality accurately and enforce actual cardinality with polynomial time complexity. We propose the range of the hyperparameter ensures that our method has no error in real implementations, based on theoretical proof and experiment. Our method applied to mathematical method outperforms baseline methods across various datasets, demonstrating the effectiveness of the identified hyperparameter.
Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT
Authors: Shuolin Li; Chu-Min Li; Jordi Coll; Djamal Habet; Felip Manyà
Venue: AAAI 2025 (main)

Abstract: The MaxSAT problem is an optimization version of the satisfiability problem (SAT). A tight lower bound (LB) on the number of falsified soft clauses in a MaxSAT solution is crucial for the efficiency of Branch-and-Bound (BnB) MaxSAT solvers. To compute an LB, modern BnB solvers detect disjoint inconsistent subsets of soft clauses, called cores, using unit propagation. A notable feature of these solvers is that soft clauses belonging to already detected cores cannot be reused to detect additional cores, limiting the number of cores that can be detected. In this paper, we propose an unlocking mechanism that allows the reuse of soft clauses in already detected cores while ensuring the soundness of LB. Experimental results show that this unlocking mechanism consistently improves the performance of a state-of-the-art BnB solver. In addition, it allowed us to win the first two places in the exact unweighted category of the MaxSAT Evaluation 2024.
Online Prompt Selection for Program Synthesis
Authors: Yixuan Li; Lewis Frampton; Federico Mora; Elizabeth Polgreen
Venue: AAAI 2025 (main)

Abstract: Large Language Models (LLMs) demonstrate impressive capabilities in the domain of program synthesis. This level of performance is not, however, universal across all tasks, all LLMs and all prompting styles. There are many areas where one LLM dominates, one prompting style dominates, or where calling a symbolic solver is a better choice than an LLM.  A key challenge for the user then, is to identify not only when an LLM is the right choice of solver, and the appropriate LLM to call for a given synthesis task, but also the right way to call it. A non-expert user who makes the wrong choice, incurs a cost both in terms of results (number of tasks solved, and the time it takes to solve them) and financial cost, if using a closed-source language model via a commercial API.  We frame this choice as an online learning problem. We use a multi-armed bandit algorithm to select which symbolic solver, or LLM and prompt combination to deploy in order to maximize a given reward function (which may prioritize solving time, number of synthesis tasks solved, or financial cost of solving). We implement an instance of this approach, called \name, and evaluate it on synthesis queries from the literature in ranking function synthesis, from the syntax-guided synthesis competition, and fresh, unseen queries generated from SMT problems. Cyanea solves 37.2 % more queries than the best single solver and achieves results within 4 % of the virtual best solver.
DiverSAT: A Novel and Effective Local Search Algorithm for Diverse SAT Problem
Authors: Jiaxin Liang; Junping Zhou; Minghao Yin
Venue: AAAI 2025 (main)

Abstract: For many real-world problems, users are often interested not only in finding a single solution but in obtaining a sufficiently diverse collection of solutions. In this work, we consider the Diverse SAT problem, aiming to find a set of diverse satisfying assignments for a given propositional formula. We propose a novel and effective local search algorithm, DiverSAT, to solve the problem. To cope with diversity, we introduce three heuristics and a perturbation strategy based on some relevant information. We conduct extensive experiments on a large number of public benchmarks, collected from semiformal hardware verification, logistics planning,  and other domains. The results show that DiverSAT outperforms the existing algorithms on most of these benchmarks.
Search Strategy Generation for Branch and Bound Using Genetic Programming
Authors: Gwen Maudet; Grégoire Danoy
Venue: AAAI 2025 (main)

Abstract: Branch-and-Bound (BB) is an exact method in integer programming that recursively divides the search space into a tree. During the resolution process, determining the next subproblem to explore within the tree—known as the search strategy—is crucial. 
Hand-crafted heuristics are commonly used, but none are effective over all problem classes. 
Recent approaches utilizing neural networks claim to make more intelligent decisions but are computationally expensive.
In this paper, we introduce GP2S (Genetic Programming for Search Strategy), a novel machine learning approach that automatically generates a BB search strategy heuristic, aiming to make intelligent decisions while being computationally lightweight. 
We define a policy as a function that evaluates the quality of a BB node by combining features from the node and the problem; the search strategy policy is then defined by a best-first search based on this node ranking. 
The policy space is explored using a genetic programming algorithm, and the policy that achieves the best performance on a training set is selected.
We compare our approach with the standard method of the SCIP solver, a recent graph neural network-based method, and handcrafted heuristics. 
Our first evaluation includes three types of primal hard problems, tested on instances similar to the training set and on larger instances. 
Our method is at most 2 percents slower than the best baseline and consistently outperforms SCIP, achieving an average speedup of 11.3 percents. Additionally, GP2S is tested on the MIPLIB 2017 dataset, generating multiple heuristics from different subsets of instances. It exceeds SCIP’s average performance in 7 out of 10 cases across 15 times more instances and under a time limit 15 times longer, with some GP2S methods leading on most experiments in terms of the number of feasible solutions or optimality gap.
Certifying Bounds Propagation for Integer Multiplication Constraints
Authors: Matthew J. McIlree; Ciaran McCreesh
Venue: AAAI 2025 (main)

Abstract: A constraint programming (CP) solver that implements proof logging will output a machine-checkable certificate of correctness alongside any result it obtains. This is useful for trusting claims of unsatisfiability or optimality, as well as for debugging and auditing solver implementations. Proofs can be constructed by having the solver log justifications for each inference it makes, and previous work has shown that many standard CP reasoning techniques can be efficiently justified using a pseudo-Boolean (PB) proof format. This paper extends PB justifications to propagators enforcing bounds consistency on multiplication and division constraints. We show that even though the proof system and checker operate only on linear inequalities over 0-1 variables, non-linear reasoning over bounded domains can be efficiently expressed as a sequence of PB proof steps. Additionally, we demonstrate that bespoke proof logging for bounds-consistency algorithms offers a clear advantage over constructing justifications by brute force.
Towards Real-Time Approximate Counting
Authors: Yash Pote; Kuldeep S. Meel; Jiong Yang
Venue: AAAI 2025 (main)

Abstract: Model counting is the task of counting the number of satisfying assignments of a Boolean formula. Since counting is intractable in general, most applications use (ε, δ)-approximations, where the output is within a (1+ε)-factor of the count with probability at least 1-δ. 
Many demanding applications make thousands of counting queries, and the state-of-the-art approximate counter, ApproxMC, makes hundreds of calls to SAT solvers to answer a single approximate counting query.
The sheer number of SAT calls, poses a significant challenge to the existing approaches. 

In this work, we propose an approximation scheme, ApproxMC7, that is tailored to such demanding applications with low time limits. Compared to ApproxMC, ApproxMC7 makes 14× fewer SAT calls while providing the same guarantees as ApproxMC in the constant-factor regime. In an evaluation over 2,247 instances, ApproxMC7 solved 271 more and achieved a 2× speedup against ApproxMC.
The Impact of Literal Sorting on Cardinality Constraint Encodings
Authors: Joseph E. Reeves; João Filipe; Min-Chien Hsu; Ruben Martins; Marijn J. H. Heule
Venue: AAAI 2025 (main)

Abstract: The effectiveness of satisfiability solvers strongly depends on the quality of the encoding of a given problem into conjunctive normal form. Cardinality constraints are prevalent in numerous problems, prompting the development and study of various types of encoding. We present a novel approach to optimizing cardinality constraint encodings by exploring the impact of literal orderings within the constraints. By strategically placing related literals nearby each other, the encoding generates auxiliary variables in a hierarchical structure, enabling the solver to reason more abstractly about groups of related literals. Unlike conventional metrics such as formula size or propagation strength, our method leverages structural properties of the formula to redefine the roles of auxiliary variables to enhance the solver's learning capabilities. The experimental evaluation on benchmarks from the maximum satisfiability competition demonstrates that literal orderings can be more influential than the choice of the encoding type. Our literal ordering technique improves solver performance across various encoding techniques, underscoring the robustness of our approach.
Computationally Hard Problems Are Hard for QBF Proof Systems Too
Authors: Agnes Schleitzer; Olaf Beyersdorff
Venue: AAAI 2025 (main)

Abstract: There has been tremendous progress in the past decade in the
field of quantified Boolean formulas (QBF), both in practical
solving as well as in creating a theory of corresponding proof
systems and their proof complexity analysis. Both for solving
and for proof complexity, it is important to have interesting
formula families on which we can test solvers and gauge the
strength of the proof systems. There are currently few such
formula families in the literature.
We initiate a general programme how to transform computationally
hard problems (located in the polynomial hierarchy)
into QBFs hard for the main QBF resolution systems Q-Res
and QU-Res that relate to core QBF solvers. We illustrate
this general approach on three problems from graph theory
and logic. This yields QBF families that are provably hard for
Q-Res and QU-Res (without any complexity assumptions).
Decomposed Quadratization: Efficient QUBO Formulation for Learning Bayesian Network
Authors: Yuta Shikuri
Venue: AAAI 2025 (main)

Abstract: Algorithms and hardware for solving quadratic unconstrained binary optimization (QUBO) problems have made significant recent progress. This advancement has focused attention on formulating combinatorial optimization problems as quadratic polynomials. To improve the performance of solving large QUBO problems, it is essential to minimize the number of binary variables used in the objective function. In this paper, we propose a QUBO formulation that offers a bit capacity advantage over conventional quadratization techniques. As a key application, this formulation significantly reduces the number of binary variables required for score-based Bayesian network structure learning. Experimental results on 16 instances, ranging from 37 to 223 variables, demonstrate that our approach requires fewer binary variables than quadratization by orders of magnitude. Moreover, an annealing machine that implement our formulation have outperformed existing algorithms in score maximization.
Scalable Quantum-Inspired Optimization Through Dynamic Qubit Compression
Authors: Co Tran; Quoc-Bao Tran; Hy Truong Son; Thang N Dinh
Venue: AAAI 2025 (main)

Abstract: Hard combinatorial optimization problems, often mapped to Ising models, promise potential solutions with quantum advantage but are constrained by limited qubit counts in near-term devices. We present an innovative quantum-inspired framework that dynamically compresses large Ising models to fit available quantum hardware of different sizes. Thus, we aim to bridge the gap between large-scale optimization and current hardware capabilities. Our method leverages a physics-inspired GNN architecture to capture complex interactions in Ising models and accurately predict alignments among neighboring spins (aka qubits) at ground states. By progressively merging such aligned spins, we can reduce the model size while preserving the underlying optimization structure. It also provides a natural trade-off between the solution quality and size reduction, meeting different hardware constraints of quantum computing devices. Extensive numerical studies on Ising instances of diverse topologies show that our method can reduce instance size at multiple levels with virtually no losses in solution quality on the latest D-wave quantum annealers.