We present a comprehensive classical and parameterized complexity analysis of decision tree pruning operations, extending recent research on the complexity of learning small decision trees. Thereby, we offer new insights into the computational challenges of decision tree simplification, a crucial aspect of developing interpretable and efficient machine learning models. We focus on fundamental pruning operations of subtree replacement and raising, which are used in heuristics. Surprisingly, while optimal pruning can be performed in polynomial time for subtree replacement, the problem is NP-complete for subtree raising. Therefore, we identify parameters and combinations thereof that lead to fixed-parameter tractability or hardness, establishing a precise borderline between these complexity classes. For example, while subtree raising is hard for small domain size $D$ or number $d$ of features, it can be solved in $D^{2d} \cdot |I|^{O(1)}$ time, where $|I|$ is the input size. We complement our theoretical findings with preliminary experimental results, demonstrating the practical implications of our analysis.

These tools apply basic strategies that work well for random problems but miss critical patterns in structured instances. SAT encodings of real problems contain inherited patterns from graph layouts, data connections, and domain-specific rules. The transformation to Conjunctive Normal Form (CNF) obscures these patterns. Current local search methods skip these structures in favor of general approaches. This paper addresses these limitations by introducing a framework that leverages LLMs to generate local search strategies tailored to encoding structures, enabling solvers to take advantage of these patterns for improved performance. Our research addresses three questions: 1. How can LLMs analyze PySAT [Ignatiev et al., 2024] code to interpret how problem structure translates to SAT clauses? 2. How can we create local search strategies that recognize and exploit these encoding patterns?

Circuits in deterministic decomposable negation normal form (d-DNNF) are representations of Boolean functions that enable linear-time model counting. This paper strengthens our theoretical knowledge of what classes of functions can be efficiently transformed, or compiled, into d-DNNF. Our main contribution is the fixed-parameter tractable (FPT) compilation of conjunctions of specific constraints parameterized by incidence treewidth. This subsumes the known result for CNF. The constraints in question are all functions representable by constant-width ordered binary decision diagrams (OBDDs) for all variable orderings. For instance, this includes parity constraints and cardinality constraints with constant threshold. The running time of the FPT compilation is singly exponential in the incidence treewidth but hides large constants in the exponent. To balance that, we give a more efficient FPT algorithm for model counting that applies to a sub-family of the constraints and does not require compilation.

Propositional satisfiability (SAT) solvers based on conflict-driven clause learning can solve huge instances with millions of variables and clauses [Fichte et al., 2023a]. However, for hard instances, particularly in combinatorial problems, parallelization becomes necessary. The cube-and-conquer technique has proven highly effective for such problems, most notably in resolving the Pythagorean triples conjecture [Heule et al., 2016]. In cube-and-conquer, a look-ahead solver first partitions the search space into disjoint subproblems via cubes (partial assignments), which are then solved independently by CDCL solvers. This independence enables efficient parallel solving. When encoding combinatorial problems into SAT, particularly those involving graphs, we often encounter highly symmetric search spaces. Many mutually isomorphic graphs satisfy the same constraints, but a solver needs to check only one representative, the canonical element, from each isomorphism class. Standard CDCL solvers cannot leverage these symmetries, and static symmetry breaking methods cannot break all symmetries [Codish et al., 2019]. SAT Modulo Symmetries (SMS) [Kirchweger and Szeider, 2021; Kirchweger and Szeider, 2024] addresses this limitation through dynamic symmetry breaking, using a custom propagator that learns symmetry-breaking predicates during the search.

While Large Language Models (LLMs) perform exceptionally well at natural language tasks, they often struggle with precise formal reasoning and the rigorous specification of problems. We present MCP-Solver, a prototype implementation of the Model Context Protocol that demonstrates the potential for systematic integration between LLMs and constraint programming systems. Our implementation provides interfaces for the creation, editing, and validation of a constraint model. Through an item-based editing approach with integrated validation, the system ensures model consistency at every modification step and enables structured iterative refinement. The system handles concurrent solving sessions and maintains a persistent knowledge base of modeling insights. Initial experiments suggest that this integration can effectively combine LLMs' natural language understanding with constraint-solving capabilities. Our open-source implementation is proof of concept for integrating formal reasoning systems with LLMs through standardized protocols. While further research is needed to establish comprehensive formal guarantees, this work takes a first step toward principled integration of natural language processing with constraint-based reasoning.

SAT modulo symmetries (SMS) is a recently proposed framework that brings efficient symmetry breaking to conflict-driven (CDCL) SAT solvers and has achieved state-of-the-art results on several symmetry-rich combinatorial search problems, enumerating or proving the non-existence of graphs, planar graphs, directed graphs, and matroids with particular properties [Kirchweger and Szeider, 2021; Kirchweger et al., 2022, 2023b]. In this paper, we propose to extend SMS to a class of problems that do not admit a succinct SAT encoding because they involve quantifier alternation: where we are asked to find a combinatorial object (the existential part) that has some co-NP-complete property (the universal part, stated as'all candidate polynomial-size witnesses fail'). We call such problems alternating search problems; a simple concrete example of an alternating search problem is the well-studied question posed by Erdős [1967], of finding a smallest triangle-free graph that is not properly k-colorable, for a fixed k 3. Encoding the non-k-colorability property for k 3 into a family of polynomially sized propositional formulas is impossible unless NP = co-NP, since checking k-colorability is NP-complete [Karp, 1972]. SMS has some advantages over alternative methods such as isomorphism-free exhaustive enumeration by canonical construction path [McKay, 1998] as implemented in tools like Nauty [McKay and Piperno, 2014], or different symmetry-breaking methods for SAT. The former can very efficiently generate all objects of a given order, but is very difficult to integrate with complex constraints and learning, while the latter is either intractable (full'static' symmetry breaking [Codish et al., 2016; Itzhakov and Codish, 2015], which requires constraints of exponential size), or ineffective (partial static symmetry breaking [Codish et al., 2019]).

Treewidth and hypertree width have proven to be highly successful structural parameters in the context of the Constraint Satisfaction Problem (CSP). When either of these parameters is bounded by a constant, then CSP becomes solvable in polynomial time. However, here the order of the polynomial in the running time depends on the width, and this is known to be unavoidable; therefore, the problem is not fixed-parameter tractable parameterized by either of these width measures. Here we introduce an enhancement of tree and hypertree width through a novel notion of thresholds, allowing the associated decompositions to take into account information about the computational costs associated with solving the given CSP instance. Aside from introducing these notions, we obtain efficient theoretical as well as empirical algorithms for computing threshold treewidth and hypertree width and show that these parameters give rise to fixed-parameter algorithms for CSP as well as other, more general problems. We complement our theoretical results with experimental evaluations in terms of heuristics as well as exact methods based on SAT/SMT encodings.

The last decades have brought enormous technological progress and innovation. Two main factors that are undoubtedly key to this development are (i) hardware advancement and (ii) algorithm advancement. Moore's Law, the prediction made by Gordon Moore in 1965 [55], that the number of components per integrated circuit doubles every year, has shown to be astonishingly accurate for several decades. Given such an exponential improvement on the hardware side, one is tempted to overlook the progress made on the algorithmic side. This paper aims to compare the impact of hardware advancement and algorithm advancement based on a genuine problem, the propositional satisfiability problem (SAT).

Bayesian network structure learning is the notoriously difficult problem of discovering a Bayesian network (BN) that optimally represents a given set of training data [4]. Since the exact inference on a BN is exponential in the BN's treewidth [14], one is particularly interested in learning BNs of bounded treewidth. However, learning a BN of bounded treewidth that optimally fits the data (i.e., with the largest possible score) is, in turn, an NPhard task [13]. This predicament caused the research on treewidth-bounded BN structure learning to split into two branches: 1. Heuristic Learning (see, e.g., [5, 17, 23, 24]), which is scalable to large BNs with thousands of nodes (but with a score that can be far from optimal), and 2. Exact Learning (see, e.g., [2, 13, 19]), which learns optimal BNs (but is scalable only to a few dozen nodes). In this paper, we combine heuristic and exact learning and take the best of both worlds.

Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We introduce dependency learning, a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. We show that dependency learning can achieve exponential speedups over ordinary QCDCL. Experiments on standard benchmark sets demonstrate the effectiveness of this technique.