ABSTRACT. Temporal Synthesis studies the automatic synthesis of interactive programs (technically called strategies) from declarative specifications expressed in temporal logic. In this talk, we show how Temporal Synthesis provides a principled foundation for strategic reasoning in autonomous AI systems, leading to what we may call Symbolic Coding Agents. Symbolic Coding Agents use temporal synthesis to generate symbolic code, including strategies, guard rails, and decision-making monitors, thereby grounding deliberative behavior in logical specifications. The key to this research path lies in the rich body of concepts developed in reasoning about actions and planning, combined with a precise treatment of nondeterministic environments and temporal objectives. In such settings, plans must be treated as strategies rather than being blurred with individual execution traces, and goal satisfaction evolves during execution rather than being reducible to reaching states with fixed properties. These features are naturally captured within the temporal synthesis framework underlying Symbolic Coding Agents. Technically, we focus on synthesis from Linear Temporal Logic on finite traces (LTLf). LTLf specifications compile into deterministic finite automata (DFAs), which can be viewed as two-player game arenas, yielding efficient and scalable synthesis procedures. We then lift these finite-trace results to infinite traces through the Manna–Pnueli hierarchy, introducing LTLf+ and its obligation fragment while largely preserving algorithmic simplicity. Finally, we move beyond synthesizing individual strategies to analyze the space of all strategies satisfying a specification. By characterizing the set of compliant execution traces, without assuming individual strategies to be analyzable, we provide formal foundations for Symbolic Coding Agents to synthesize guard rails and decision-making monitors, as well as tools for responsibility attribution in agentic AI systems composed of multiple agents that make decisions independently.

ABSTRACT. Cumulative constraints are central in scheduling with constraint programming, yet propagation is typically performed per constraint, missing multi-resource interactions and causing severe slowdowns on some benchmarks. I present a preprocessing method for inferring additional cumulative constraints that capture such interactions without search-time probing. This approach interprets cumulative constraints as linear inequalities over occupancy vectors and generates valid inequalities by (i) discovering covers, the sets of tasks that cannot run in parallel, (ii) strengthening the cover inequalities for the discovered sets with lifting, and (iii) injecting the resulting constraints back into the scheduling problem instance. Experiments on standard RCPSP and RCPSP/max test suites show that these inferred constraints improve search performance and tighten objective bounds on favorable instances, while incurring little degradation on unfavorable ones. Additionally, these experiments discover 25 new lower bounds and five new best solutions; eight of the lower bounds are obtained directly from the inferred constraints.

ABSTRACT. Few amongst the rules that filter the Cumulative constraint reason on the integrity of resource consumption. We augment the overload check with an integral reasoning that better evaluates resource availability. This reasoning is based on the knapsack problem, which we solve using dynamic programming. Our new rule subsumes the time table horizontally elastic overload check while its running time complexity is O(Cn^2), only increasing by a factor C (the resource capacity) due to solving knapsack problems. Our algorithm generates explanations for lazy clause generation solvers. With our new knapsack augmented overload check, we are able to solve all but 5 instances of the Pack benchmark. By performing a small transformation of the instances, we show that our method is more robust than known pre-solving methods that perform well on the original benchmark.

ABSTRACT. Optional variables have for a long time been identified as a crucial component of state-of-the-art scheduling solvers. They not only offer a natural way to model many scheduling problems but also play an important role in the efficiency of such solvers by enabling a stronger inference in a constraint propagation engine. Despite this recognition, their adoption in modern solvers remains extremely scarce presumably because their native support requires pervasive changes to a solver and handling many subtleties that have not been extensively studied. In this paper, we aim to provide a good foundation in this direction by providing a formal characterization of optional variables and of their interactions with key component of constraint programming solver including propagators, reification and lazy clause generation. In addition, we present a new lazy clause generation solver with native support for optional variables and demonstrate its efficiency on variants of the flexible jobshop problem.

ABSTRACT. Benchmarking scheduling instances solely by nominal size is often misleading: instances with the same number of jobs and machines can differ by orders of magnitude in empirical hardness. This paper proposes a fully supervised, solver-aligned difficulty estimator for the Job Shop Scheduling Problem (JSP). Each instance is represented in an instance space through structural descriptors extracted from the disjunctive graph and instance-derived summaries, while supervision is obtained from normalized solver traces aggregated across OR-Tools, Gurobi, and CPLEX. A Random Forest regressor learns a bounded hardness score P(x) in [0,1], from which balanced easy/medium/hard categories are induced. The empirical evaluation shows that the learned score is strongly aligned with solver-effort indicators, provides interpretable feature-level explanations, and preserves meaningful ordinal relationships on classical JSPLIB benchmarks under distribution shift. The proposed framework provides a practical and interpretable basis for difficulty-aware benchmarking, instance selection, and solver-behaviour analysis beyond nominal size parameters.

ABSTRACT. Constraint Programming (CP) is a powerful optimization method that provides optimality guarantees, but due to its exact nature, its scalability to large instances is often limited. To address this, we propose a hybrid approach that combines a CP solver with heuristic methods, directly and asynchronously exchanging solutions and objective values during runtime. This real-time cooperation yields faster convergence to good solutions across various problem domains than the solver alone, while retaining the ability to guarantee optimality, leveraging the complementary nature of the CP solver and heuristics. The efficiency of this approach is evaluated on three well-known scheduling problems and three well-known routing problems. Noticeable improvements are observed for the Flow-shop Scheduling Problem (FSSP), the Traveling Salesman Problem (TSP), and the Vehicle Routing Problem with Time Windows (VRP-TW). Even for problems where improvements are marginal, the portfolio of methods increases the robustness of the approach.

ABSTRACT. Multi-Armed Bandit (MAB) mechanisms have proven effective for adaptive heuristic switching in modern CDCL SAT solvers, with Kissat_MAB and its variants demonstrating strong performance in recent SAT Competitions. However, while strategies like the Luby series generate restarts with high duration variability, standard bandit models treat each restart as a homogeneous unit. This mismatch can bias credit assignment and lead to suboptimal exploration–exploitation trade-offs between short and long restarts. In this paper, we study MAB-based heuristic selection under variable-duration restart policies and propose a duration-aware modification to both bandit feedback and selection mechanisms. Our approach normalizes and conditions rewards on the restarts and adapts exploration and exploitation accordingly, thereby better aligning bandit updates with the solver’s restart dynamics.

ABSTRACT. Tree ensembles (TEs) are among the most widely used machine learning models, yet explaining their predictions remains a computational challenge. Recent work in formal explainable AI (FXAI) has focused on computing abductive explanations for TEs using Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT). However, these methods often fail to scale with the growth of the number and depth of the trees in the ensemble. This paper addresses these scalability limitations by shifting focus to Rule Ensembles (REs), a structurally simpler alternative to TEs. We make three primary contributions. First, we adapt an existing MaxSAT-based explanation framework designed for TEs to function with general REs. Second, we devise a dedicated logic encoding for REs combining SAT solving with pseudo-Boolean (PB) constraints for determining the winning class. Finally, empirical experiments on standard tabular and image datasets demonstrate a significant advantage of the proposed SAT-based approach for REs over the state-of-the-art MaxSAT-based approach for TEs.

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. Conflict-Driven Clause Learning (CDCL) is central to the success of SAT solvers, and its adaptation to Constraint Programming (CP) through Lazy Clause Generation (LCG) has been a major breakthrough for CP solving. A core requirement of LCG is to maintain both a CP and SAT view of the problem. Because maintaining a full SAT encoding is impractical, solvers rely on partial and solver-specific encodings—an approach that has evolved as folklore rather than formal design. We present the first systematic analysis of how leading LCG solvers maintain their SAT encodings, based on source-code inspection and developer correspondence. Our analysis reveals substantial differences in explanation lifting, backwards explanations, linking clauses, and nogood minimisation, all driven by the need to preserve a SAT view. To overcome these compromises, we propose a native CDCL framework for CP. We replace SAT literals with atomic constraints, enabling conflict analysis, nogood learning, and nogood propagation directly at the CP level. This results in cleaner algorithmic design, eliminates SAT-specific complications, and allows us to introduce extended nogood propagation, a generalisation of SAT-based clause propagation, as well as CPIP nogoods, a generalisation of SAT-based learned nogoods. Our implementation of the framework in Solver demonstrates competitive performance in the MiniZinc Challenge 2025. Additionally, we empirically show that extended nogood propagation combined with CPIP nogoods can significantly reduce failures, especially on problems with constraints that reason over domain holes. Overall, our framework provides a principled and semantically rich generalisation of CDCL for CP.

ABSTRACT. The Large Weight Syndrome Decoding problem LWSD is a fundamental problem in coding theory. It consists in determining whether a given linear code admits a high Hamming weight vector associated with a specific syndrome. LWSD is a variant of the classical syndrome decoding problem, which conversely seeks a low Hamming weight solution for a linear system defined over the binary field $\mathbb{F}_2$. In this paper, we investigate a generalization of this problem to the case of a prime finite field $\mathbb{F}_Z$, referred to as LWZSD. We propose several models using Boolean Satisfiability (SAT) formulas and compare the efficiency of our approaches against state-of-the-art solvers.