ABSTRACT. In an era where data-driven machine learning (ML), large language models (LLMs), and agentic AI are clearly improving efficiency in solving complex problems—such as classifying images, answering questions, or playing complex games—solving NP-hard combinatorial problems remains largely dominated by long-developed methods like mathematical programming, constraint programming, or metaheuristics. In this preliminary work, we present two distinct approaches tested to tackle the RCPSP/Max problem, a classic scheduling benchmark that is notably challenging for mathematical programming to find even a feasible solution. One approach focuses on program synthesis using an evolutionary framework powered by an LLM, while the other is based on learning task ranking solutions from optimal solutions using graph neural networks (GNNs) coupled with a LLM-synthetized post-processing procedure to produce feasible schedules. We provide qualitative and empirical conclusions, discuss the true limits of LLM "creativity" and deep learning to solve challenging scheduling problems, and propose avenues for further work.

ABSTRACT. Algorithm selection is important in satisfiability and constraint solving, since no single solver performs best across all instances. Traditional learning-based approaches represent problem instances using expert-designed features to predict solver performance, while recent work explores graph representations derived from ASTs. However, most existing approaches overlook high-level contextual information, such as the application domain or the benchmark origin. In practice, such cues often help practitioners choose an appropriate solver. We present SMT-Select, a multimodal framework for SMT algorithm selection. It learns graph representations from formula ASTs and textual representations from natural-language context descriptions. These representations are then combined to guide solver selection. Evaluated across nine SMT logics, \textsc{SMT-Select} consistently outperforms existing selectors and SMT-COMP winning solvers. Across all evaluated logics, it closes at least 30% of the performance gap between the competition winner and the virtual best solver (VBS), and nearly matches the VBS in two logics.

ABSTRACT. Contrastive learning has recently emerged as a powerful paradigm for training discriminative policies by distinguishing good decisions from bad ones. In this paper, we exploit this idea to learn neighborhood selection in combinatorial optimization, specifically for the Cost Function Networks (CFNs) — a rich framework for representing a global probability distribution or energy function as a combination of local functions. A central inference task is to find a global assignment of all variables with maximum a posteriori probability, or equivalently, minimum energy. We build on \vnsldscp, an anytime incomplete method implemented in the Toulbar2 solver, whose performance hinges on selecting the right variables for repair. Rather than relying on problem-specific heuristics, we propose \clvns a pipeline that extracts positive and negative neighborhood samples from \vnsldscp search trajectories and uses them to train a Graph Neural Network (GNN) with graph attention and a contrastive objective. The resulting model learns to score variables by their relevance for improvement, and is integrated into the \vnsldscp loop to guide the neighborhood construction at inference time. We evaluate the proposed approach on \cfn instances, including challenging minimum-energy problems arising in Computational Protein Design. Experimental results show that \clvns consistently improves solution quality over time compared to the standard \vnsldscp baseline, demonstrating the promise of contrastive learning for guiding combinatorial search.

ABSTRACT. Anytime MaxSAT solving is indispensable in applications that require finding near-optimal solutions within a flexible, user-controlled time budget. Recent years have seen substantial progress in anytime MaxSAT algorithms, including the introduction of SAT-based local search, the development of efficient approximation techniques, and significant advances in classical local search methods. However, all leading anytime solvers—including the winners of the three most recent MaxSAT Evaluations (MSEs) in the anytime categories—reuse the code base of a single solver, tt-open-wbo-inc. While highly efficient, this code base lacks an in-memory API, is non-incremental and incomplete, and contains a substantial amount of dead and legacy code. We introduce Aperture, a new solver for SAT-based optimization, including MaxSAT, written from scratch in C++ with in-memory APIs for C++ (IPAMIR-compliant) and Python. For MaxSAT, Aperture is anytime, incremental, and complete; algorithmically, it follows a similar high-level approach to tt-open-wbo-inc, but employs a unified flow for both weighted and unweighted MaxSAT. Performance-wise, Aperture is highly competitive as a MaxSAT solver. Under the benchmark sets and evaluation conditions of MSE 2024, it outperforms both the MSE 2024 winner SPB-MaxSAT-c and tt-open-wbo-inc in all four anytime categories, and in 8 out of 12 anytime categories across the three most recent MSEs (2022–2024). Moreover, Aperture outperforms leading non-anytime MaxSAT solvers on 2 out of the 6 incremental benchmark sets from MSE 2022, an evaluation setting in which—unlike the anytime categories—both incrementality and completeness are mandatory. Beyond MaxSAT, Aperture also supports other paradigms for optimizing an objective function under Boolean constraints, including Optimization Modulo Bitvectors (OBV) and black-box optimization. Across all supported paradigms, the solver is incremental and anytime; it is complete for MaxSAT and OBV, but incomplete for black-box optimization.

ABSTRACT. Implicit Hitting Set (IHS) Solving has been a successful solving paradigm in maximum satisfiability (MaxSAT) and has also recently been ported to pseudo-Boolean optimization (PBO). In a nutshell, the IHS algorithm iteratively solves an underconstrained version of the original optimization problem, which we refer to as the hitting set (HS) problem. A solution to the hitting set problem is then attempted to be extended to a solution to the original problem. If the solution cannot be extended, a new constraint is added to the hitting set problem. Traditionally, the hitting set problem has been solved using an integer linear programming solver. We propose instead using the pseudo-Boolean solver RoundingSat, which supports VeriPB proof logging, as well as local search, to solve the HS problem. This allowed us, for the first time, to provide a certifying IHS solver, which participated in the Pseudo-Boolean Competition 2025. However, it is very challenging to create a certifying IHS solver that is competitive with uncertified IHS solving. This is evident in the concurrent work (Ihalainen et al., AAAI 2026), where introducing certification results in a major hit in performance. The hitting set solver is being run on a problem with a growing number of constraints, and a major challenge is how to recycle information between calls rather than solving the HS problem from scratch every time. Our solution is to use additional activation variables to keep track of which constraints remain valid in between calls, but adapting solver heuristics and constraint post-processing techniques to this setting is highly nontrivial. In our presentation, we will explain some of the technical challenges involved and then report on experimental results from our work-in-progress implementation in the solver RoundingSat, which shows that proofs for all solved instances can be verified by VeriPB and the formally verified checker CakePB. Our preliminary experiments show that performance can be made competitive with uncertified IHS solving with SCIP as the hitting set solver.

ABSTRACT. Maximum Satisfiability (MaxSAT) is an optimization extension of the Satisfiability (SAT) problem. In Branch-and-Bound (BnB) MaxSAT solving, the quality of the lower bound estimation is critical for effective search space pruning. State-of-the-art BnB solvers typically estimate this bound by identifying disjoint inconsistent subformulas (cores) via Unit Propagation (UP). However, a limitation of this standard approach is that UP fails to detect cores that exhibit complex dependencies with already identified cores. In this paper, we propose a further lookahead algorithm that leverages pre-detected cores to uncover additional disjoint inconsistencies, thereby tightening the lower bound. Experimental results demonstrate that the proposed algorithm significantly tightens the lower bound, enabling the state of the art BnB solver MaxCDCL to solve more instances.

ABSTRACT. Constraint satisfaction problems underlie many resource allocation and scheduling decisions. When feasible solutions affect individual stakeholders, a solver that returns a single high-quality solution may systematically favor some individuals over others, even when many equally valid solutions exist. In this paper we address fair decision making for combinatorial optimization problems of the kind routinely solved with popular frameworks such as SAT solvers, constraint programming, or integer programming. We study (first-level) distributional max-min fairness for constraint satisfaction problems, whereby the solver outputs a probability distribution over feasible solutions that maximizes the expected utility of the least-favored stakeholder. We propose an approximate algorithm based on the multiplicative weights update framework, where each iteration calls an oracle for a weighted version of the original CSP. Preliminary experiments with a variety of solvers show that our approach can be practical on NP-hard benchmark problems for which state-of-the-art solvers are effective.

ABSTRACT. Pseudo-Boolean solving adapts the revolutionary conflict-driven clause learning (CDCL) algorithm from Boolean satisfiability (SAT) to the much more expressive paradigm of 0-1 integer linear programming. Conflict analysis for 0-1 integer linear programming requires applying cuts to constraints, which transform constraints to constraints that are implied over the Booleans but not necessarily over the reals. It also requires weakening constraints, which focuses constraints more on the conflict and can make cuts more effective. In this work-in-progress paper, we systematically study a number of different cut rules and different methods to weaken constraints. Our preliminary experimental evaluation agrees with some theoretical expectations, but also provides some unexpected results and shows that different benchmark families benefit from different cut rules.

ABSTRACT. The Quadratic Assignment Problem (QAP) consists of finding a permutation that minimizes a quadratic objective function. Exact methods generally rely on a branch-and-bound procedure, the efficiency of which depends heavily on the quality of its lower bound. In integer linear programming, several bounds have been investigated, exhibiting different trade-offs between speed and quality. The Gilmore-Lawler bound appears to be the most commonly used in practice. It requires solving a linear assignment problem (LAP) for each variable-value pair. We show how to obtain this bound using Singleton Node Consistency (SNC) and LAP. In Cost Function Networks (CFNs), we propose a reformulation that transforms the result of applying LAP to a given variable-value pair into cost functions of arity 1 and 2, which can be added to the original problem. Combined with existing lower bounds for CFNs, including EDAC and a recent CFN propagator for AllDifferent, this method (SNC-LAP-GLB), used as a preprocessing, significantly increases the initial lower bound and accelerates the search, resulting in competitive results on the QAPLIB benchmark. We then propose an extension of the AllDifferent propagator for the Global Cardinality Constraint. It allows us to exploit variable symmetries on some challenging QAPLIB instances, thus improving the results. Last, we report some preliminary results obtained by an automatic configuration tool for tuning the solver parameters.