GenAI4ELab/papercli-papers huggingface dataset:
Ordered Objectives in Maximum Satisfiability
Authors: Jeremias Berg; André Schidler; Matti Järvisalo
Venue: AAAI 2026 (main)

Abstract: Maximum satisfiability (MaxSAT) is a viable approach to solving NP-hard combinatorial optimization problems through propositional encodings. Understanding how problem structure and encodings impact the behaviour of different MaxSAT solving algorithms is an important challenge. In this work, we identify MaxSAT instances in which the constraints entail an ordering of the objective variables as an interesting instance class from the perspectives of problem structure and MaxSAT solving. From the problem structure perspective, we show that a non-negligible percentage of instances in commonly used MaxSAT benchmark sets have ordered objectives and further identify various examples of such problem domains to which MaxSAT solvers have been successfully applied. From the algorithmic perspective, we argue that MaxSAT instances with ordered objectives, provided an ordering, can be solved (at least) as efficiently with a very simplistic algorithmic approach as with modern core-based MaxSAT solving algorithms. We show empirically that state-of-the-art MaxSAT solvers suffer from overheads and are outperformed by the simplistic  approach on real-world optimization problems with ordered objectives.
Proof Systems for Tensor-based Model Counting
Authors: Olaf Beyersdorff; Joachim Giesen; Andreas Goral; Tim Hoffmann; Kaspar Kasche; Christoph Staudt
Venue: AAAI 2026 (main)

Abstract: Solving the model counting problem #SAT, asking for the number of satisfying assignments of a propositional formula, has been explored intensively and has gathered its own community. While most existing solvers are based on knowledge compilation, another promising approach is through contraction in tensor hypernetworks. 
We perform a theoretical proof-complexity analysis of this approach. For this, we design two new tensor-based proof systems that we show to tightly correspond to tensor-based #SAT solving. We determine the simulation order of #SAT proof systems and prove exponential separations between the systems. This sheds light on the relative performance of different #SAT solving approaches.
Proof Systems That Tightly Characterise Model Counting Algorithms
Authors: Olaf Beyersdorff; Tim Hoffmann; Kaspar Kasche
Venue: AAAI 2026 (main)

Abstract: Several proof systems for model counting have been introduced in recent years, mainly in an attempt to model #SAT solving and to allow proof logging of solvers. We reexamine these different approaches and show that: 
(i) with moderate adaptations, the conceptually quite different proof models of the dynamic system MICE and the static system of annotated Decision-DNNFs are equivalent and 
(ii) they tightly characterise state-of-the-art #SAT solving. 
Thus, these proof systems provide a precise and robust proof-theoretic underpinning of current model counting. We also propose new strengthenings of these proof systems that might lead to stronger model counters.
Using Certifying Constraint Solvers for Generating Step-wise Explanations
Authors: Ignace Bleukx; Maarten Flippo; Bart Bogaerts; Emir Demirović; Tias Guns
Venue: AAAI 2026 (main)

Abstract: In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable.
A recently proposed method for this is to compute a sequence of explanation steps.
Such a step-wise explanation shows individual reasoning steps involving constraints from the original specification, that in the end explain a conflict.
However, computing a step-wise explanation is computationally expensive, limiting the scope of problems for which it can be used.
We investigate how we can use proofs generated by a constraint solver as a starting point for computing step-wise explanations, instead of computing them step-by-step.
More specifically, we define a framework of abstract proofs, in which \textit{both} proofs and step-wise explanations can be represented.
We then propose several methods for converting a proof to a step-wise explanation sequence, with special attention to trimming and simplification techniques to keep the sequence and its individual steps small.
Our results show our method significantly speeds up the generation of step-wise explanation sequences, while the resulting step-wise explanation has a quality similar to the current state-of-the-art.
Learning DFAs from Positive Examples Only via Word Counting
Authors: Benjamin Bordais; Daniel Neider
Venue: AAAI 2026 (main)

Abstract: Learning finite automata from positive examples has recently gained attention as a powerful approach for understanding, explaining, analyzing, and verifying black-box systems. The motivation for focusing solely on positive examples arises from the practical limitation that we can only observe what a system is capable of (positive examples) but not what it cannot do (negative examples). Unlike the classical problem of passive DFA learning with both positive and negative examples, which has been known to be NP-complete since the 1970s, the topic of learning DFAs exclusively from positive examples remains poorly understood. This paper introduces a novel perspective on this problem by leveraging the concept of counting the number of accepted words up to a carefully determined length. Our contributions are twofold. First, we prove that computing the minimal number of words up to this length accepted by DFAs of a given size that accept all positive examples is NP-complete, establishing that learning from positive examples alone is computationally demanding. Second, we propose a new learning algorithm with a better asymptotic runtime than the best-known bound for existing algorithms. While our experimental evaluation reveals that this algorithm under-performs state-of-the-art methods, it demonstrates significant potential as a preprocessing step to enhance existing approaches.
Aperiodic Tiling and Rhythmic Canons: A CP Journey
Authors: Guillaume Derval; Christophe Lecoutre
Venue: AAAI 2026 (main)

Abstract: The Aperiodic Tiling Complements Problem (ATCP) involves finding the full set of (normalized) aperiodic complements of a given pattern.
This has become a classic problem in music theory, with some recent attempts to model it using Integer Linear Programming (ILP) and Boolean Satisfiability (SAT) frameworks.
In this paper, we develop and compare different models of ATCP encoded with Constraint Programming (CP).
The most effective approach admits two phases: a first one that allows us to merge (join) several subsets of linear constraints under the form of tables with large arity, and a second one that advantageously exploits the generated tables to discard periodic tiling complements.
Our experimental results show that our approach significantly outperforms the state-of-the-art, solving every instance of a classical benchmark (standard Vuza rhythms for canons with periods set up to 900) in a time between 5 seconds and 2 minutes (except the largest instance being solved in 18 minutes).
Exact Algorithms for Distance to Unique Vertex Cover
Authors: Foivos Fioravantes; Dušan Knop; Nikolaos Melissinos; Michal Opler; Manolis Vasilakis
Venue: AAAI 2026 (main)

Abstract: In their AAAI 2024 paper, Horiyama et al. studied the problem of generating graph instances that possess a unique minimum vertex cover under specific conditions. Their approach involved pre-assigning certain vertices to be part of the solution or excluding them from it. Notably, for the Vertex Cover problem, pre-assigning a vertex is equivalent to removing it from the graph. Horiyama et al. focused on maintaining the size of the minimum vertex cover after these modifications. In this work, we extend their study by relaxing this constraint: 
our goal is to ensure a unique minimum vertex cover, even if the removal of a vertex may not incur a decrease on the size of said cover.

Surprisingly, our relaxation introduces significant theoretical challenges.
We observe that the problem is Σ²_P-complete, and remains so even for planar graphs of maximum degree 5.
Nevertheless, we provide a linear time algorithm for trees, which is then further leveraged to show that MU-VC is in FPT when parameterized by the combination of treewidth and maximum degree. Finally, we show that MU-VC is in XP when parameterized by clique-width while it is fixed-parameter tractable (FPT) if we add the size of the solution as part of the parameter.
Preference Elicitation for Step-Wise Explanations in Logic Puzzles
Authors: Marco Foschini; Marianne Defresne; Emilio Gamba; Bart Bogaerts; Tias Guns
Venue: AAAI 2026 (main)

Abstract: Step-wise explanations can explain logic puzzles and other satisfaction problems by showing how to derive decisions step by step. Each step consists of a set of constraints that derive an assignment to one or more decision variables. However, many candidate explanation steps exist, with different sets of constraints and different decisions they derive. To identify the most comprehensible one, a user-defined objective function is required to quantify the quality of each step. However, defining a good objective function is challenging. Here, interactive preference elicitation methods from the wider machine learning community can offer a way to learn user preferences from pairwise comparisons. We investigate the feasibility of this approach for step-wise explanations and address several limitations that distinguish it from elicitation for standard combinatorial problems. First, because the explanation quality is measured using multiple sub-objectives that can vary a lot in scale, we propose two dynamic normalization techniques to rescale these features and stabilize the learning process. We also observed that many generated comparisons involve similar explanations. For this reason, we introduce MACHOP (Multi-Armed CHOice Perceptron), a novel query generation strategy that integrates non-domination constraints with upper confidence bound-based diversification. We evaluate the elicitation techniques on Sudokus and Logic-Grid puzzles using artificial users, and validate them with a real-user evaluation. In both settings, MACHOP consistently produces higher-quality explanations than the standard approach.
Model Counting for Dependency Quantified Boolean Formulas
Authors: Long-Hin Fung; Che Cheng; Jie-Hong Roland Jiang; Friedrich Slivovsky; Tony Tan
Venue: AAAI 2026 (main)

Abstract: Dependency Quantified Boolean Formulas (DQBF) generalize QBF by explicitly specifying which universal variables each existential variable depends on, instead of relying on a linear quantifier order. The satisfiability problem of DQBF is NEXP-complete, and many hard problems can be succinctly encoded as DQBF. Recent work has revealed a strong analogy between DQBF and SAT: k-DQBF (with k existential variables) is a succinct form of k-SAT, and satisfiability is NEXP-complete for 3-DQBF but PSPACE-complete for 2-DQBF, mirroring the complexity gap between 3-SAT (NP-complete) and 2-SAT (NL-complete).

Motivated by this analogy, we study the model counting problem for DQBF, denoted #DQBF. Our main theoretical result is that #2-DQBF is #EXP-complete, where #EXP is the exponential-time analogue of #P. This parallels Valiant's classical theorem stating that #2-SAT is #P-complete. As a direct application, we show that first-order model counting (FOMC) remains #EXP-complete even when restricted to a PSPACE-decidable fragment of first-order logic and domain size two.

Building on recent successes in reducing 2-DQBF satisfiability to symbolic model checking, we develop a dedicated 2-DQBF model counter. Using a diverse set of crafted instances, we experimentally evaluated it against a baseline that expands 2-DQBF formulas into propositional formulas and applies propositional model counting.  While the baseline worked well when each existential variable depends on few variables, our implementation scaled significantly better to larger dependency sets.
Constraint Optimization of MicroPlate Designs
Authors: Ramiz Gindullin; María Andreína Francisco Rodríguez
Venue: AAAI 2026 (main)

Abstract: Standardized microplates are used to conduct large-scale biomedical research. The design of microplate layouts plays an essential role in handling so-called plate effects, i.e., systematic variations across the geometry of a microplate. An effective layout allows us to detect and negate plate effects. The randomized placement of controls and compounds produces layouts of limited effectiveness, so specific approaches are needed. A previously developed system, PLAID, proposed a constraint satisfaction model to construct effective plate layouts. However, PLAID does not scale well with microplate dimensions. To improve on PLAID, we propose Constraint Optimization of MicroPlate Designs (COMPD), which allows for greater flexibility and higher quality of the layouts.
Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach
Authors: Hannes Ihalainen; Dieter Vandesande; André Schidler; Jeremias Berg; Bart Bogaerts; Matti Järvisalo
Venue: AAAI 2026 (main)

Abstract: The implicit hitting set (IHS) approach offers a general framework for solving computationally  hard combinatorial optimization problems declaratively. IHS iterates between a decision oracle used for extracting sources of inconsistency and an optimizer for computing so-called hitting sets (HSs) over the accumulated sources of inconsistency. While the decision oracle is language-specific, the optimizers is usually instantiated through integer programming.

We explore alternative algorithmic techniques for hitting set optimization based on different ways of employing pseudo-Boolean (PB) reasoning as well as stochastic local search. We extensively evaluate the practical feasibility of the alternatives in particular in the context of pseudo-Boolean (0-1 IP) optimization as one of the most recent instantiations of IHS. Highlighting a trade-off between efficiency and reliability, while a commercial IP solver turns out to remain the most effective way to instantiate HS computations, it can cause correctness issues due to numerical instability; in fact,  we show that exact HS computations instantiated via PB reasoning can be made competitive with a numerically exact IP solver. Furthermore, the use of PB reasoning as a basis for HS computations allows for obtaining certificates for the correctness of IHS computations, generally applicable to any IHS instantiation in which reasoning in the declarative language at hand can be captured in the PB-based proof format we employ.
The Limitations and Power of NP-Oracle Based Functional Synthesis Techniques
Authors: Brendan Juba; Kuldeep S. Meel
Venue: AAAI 2026 (main)

Abstract: Given a Boolean relational specification between inputs and outputs, the 
problem of functional synthesis is to construct a function that maps each 
assignment of the input to an assignment of the output such that each tuple 
of input and output assignments meets the specification. The past decade has 
	witnessed significant improvement in the scalability of 
	functional synthesis tools, allowing them to handle problems with tens 
	of thousands of variables. A common ingredient in these approaches is their 
	reliance on SAT solvers, thereby exploiting the breakthrough advances in SAT 
	solving over the past three decades. While the recent techniques have been 
	shown to perform well in practice, there is little theoretical understanding 
	of the limitations and power of these approaches.	

The primary contribution of this work is to initiate a systematic theoretical investigation into the power of functional synthesis approaches that rely on NP oracles. We first  show that even when small Skolem functions exist, naive bit-by-bit learning approaches fail 
due to the relational nature of specifications. We establish fundamental limitations of interpolation-based 
	approaches  proving that even when  small Skolem functions exist, resolution-based interpolation must produce 
	exponential-size circuits. We prove that access to an NP oracle is inherently necessary for efficient synthesis.  Our main technical result shows that it is possible to use NP oracles to synthesize small Skolem functions in time polynomial  in the size of the specification and the size of the smallest sufficient set of witnesses, establishing positive results for a broad class of relational  specifications.
Graph Choosability via SAT: Beyond the Nullstellensatz
Authors: Markus Kirchweger; Tomáš Peitl; David Seka; Stefan Szeider
Venue: AAAI 2026 (main)

Abstract: List coloring extends graph coloring by assigning each vertex a list of allowed colors.
A graph is k-choosable if it can be properly colored for any choice of lists with k colors each.
Deciding k-choosability is π²ₚ-complete, bipartite graphs have unbounded list chromatic number, and planar graphs (famously 4-colorable) are all 5-choosable but not all 4-choosable.

To search for graphs of given choosability, we extend SAT Modulo Symmetries (SMS) with custom propagators
for list coloring pruning techniques and propose a quantified Boolean (QBF) encoding for choosability.
We employ a hybrid approach: pen-and-paper reasoning to optimize our formulas followed by automated case distinction by QBF solvers and SMS.

Our methods yield two significant results: (1) a 27-vertex planar graph that is 4-choosable yet cannot be proven so using the combinatorial Nullstellensatz widely applied in previous work (we show this is a smallest graph with that property), and (2) the smallest graph exhibiting a gap between chromatic and list chromatic numbers for chromatic number 3.
Using Constraint Solvers to Construct Binary Codes with Good Error Correction Performance
Authors: Stepan Kochemazov; Oleg Zaikin; Grigorii Trofimiuk; Kirill Antonov; Alexander Semenov
Venue: AAAI 2026 (main)

Abstract: In recent years, constraint solvers show increasing use in solving various open combinatorial problems, e.g., from Ramsey theory or synthesis of combinatorial designs. The similar approach can be applied to some problems related to binary linear codes, which form one of the largest families of error correcting codes used both in coding theory and in various practical applications. Thanks to a simple algebraic structure of such codes it is possible to study them using a wide range of methods. Note that even codes with the same basic parameters (length n, dimension k, minimum code distance d) can show different error correction performance, i.e., the ability to correct errors which appear in a noisy channel. In the paper, we formulate the problem of finding binary linear codes with good error correction performance as a constraint optimization problem and explore the effectiveness of modern constraint solvers on it, including SAT, MaxSAT, and CP solvers. Using the respective solvers and parallel computing, for several values of n, k, d we found the codes which are significantly better than the known in terms of their practical performance.
Towards Single Exponential Time for Temporal and Spatial Reasoning: A Study via Redundancy and Dynamic Programming
Authors: Victor Lagerkvist; Johanna Groven; Leif Eriksson
Venue: AAAI 2026 (main)

Abstract: The region connection calculus (RCC) and Allen's interval algebra (IA) are two well-known NP-hard spatial-temporal qualitative reasoning problems. They are solvable in 2^(O(n log n)) time, where n is the number of variables, and IA is additionally known to be solvable in o(n)^n time. However, no improvement over exhaustive search is known for RCC, and if they are also solvable in single exponential time 2^O(n) is unknown. We investigate multiple avenues towards reaching such bounds. First, we show that branching is insufficient since there are too many non-redundant constraints. Concretely, we classify the maximum number of non-redundant constraints in RCC and IA. Algorithmically, we make two significant contributions based on dynamic programming (DP). The first algorithm runs in 4^n time and is applicable to a non-trivial, NP-hard fragment of IA, which includes the well-known interval graph sandwich problem of (Golumbic and Shamir 1993). For the richer RCC problem with 8 basic relations we use a more sophisticated approach which asymptotically matches the o(n)^n bound for IA.
Scale-Net: A Hierarchical U-Net Framework for Cross-Scale Generalization in Multi-Task Vehicle Routing
Authors: Suyu Liu; Zhiguang Cao; Nan Yin; Yew-Soon Ong
Venue: AAAI 2026 (main)

Abstract: Neural solvers for Vehicle Routing Problems (VRPs) have shown great advantages in solving various kinds of problem types. However, they also face critical challenges in generalizing from small-scale training to large-scale problems and in identifying the most salient topological information for decision-making. To mitigate these gaps, we introduce ScaleNet, a novel hierarchical framework that integrates a U-Net architecture into a unified, multi-task VRP solver. Scale-Net explicitly captures multi-scale structural patterns by processing a nested hierarchy of input graph instances. This enriched, coarse-to-fine representation is extracted by the encoder and fed directly into the decoder, empowering decoder module with superior topological awareness for routing decisions while simultaneously reducing computational overhead in the encoder. We conducted extensive experiments on 16 VRP variants with instances ranging from 50 to 5,000 nodes. The experimental results show that Scale-Net demonstrates significant performance gains over state-of-the-art baselines across in-distribution, zero-shot, and real-world settings.
LLM-Guided Quantified SMT Solving over Uninterpreted Functions
Authors: Kunhang Lv; Yuhang Dong; Rui Han; Fuqi Jia; Feifei Ma; Jian Zhang
Venue: AAAI 2026 (main)

Abstract: Quantified formulas with Uninterpreted Functions (UFs) over non-linear real arithmetic pose fundamental challenges for Satisfiability Modulo Theories (SMT) solving. Traditional quantifier instantiation methods struggle because they lack semantic understanding of UF constraints, forcing them to search through unbounded solution spaces with limited guidance. We present AquaForte, a framework that leverages Large Language Models to provide semantic guidance for UF instantiation by generating instantiated candidates for function definitions that satisfy the constraints, thereby significantly reducing the search space and complexity for solvers. Our approach preprocesses formulas through constraint separation, uses structured prompts to extract mathematical reasoning from LLMs, and integrates the results with traditional SMT algorithms through adaptive instantiation. AquaForte maintains soundness through systematic validation: LLM-guided instantiations yielding SAT solve the original problem, while UNSAT results generate exclusion clauses for iterative refinement. Completeness is preserved by fallback to traditional solvers augmented with learned constraints. Experimental evaluation on SMT-COMP benchmarks demonstrates that AquaForte solves numerous instances where state-of-the-art solvers like Z3 and CVC5 timeout, with particular effectiveness on satisfiable formulas. Our work shows that LLMs can provide valuable mathematical intuition for symbolic reasoning, establishing a new paradigm for SMT constraint solving.