Konstantin Sidorov

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 exhibiting more stable performance on unfavorable instances than the prior work. Additionally, these experiments discover 25 new lower bounds and five new best solutions; seven of the lower bounds are obtained directly from the inferred constraints.

Constraint programming solvers have seen much success in scheduling problems owing to their efficient reasoning over constraints to solve complex problems in practice. Many algorithms have been proposed for propagating information from a single constraint. However, inferring and exchanging information across multiple constraints can provide deeper insight into the global structure of a problem. In this work, we propose to exchange information amongst constraints by inferring the disjointness of tasks in scheduling problems from many constraints. We do this by (i) augmenting existing propagators, such as the Cumulative and nogoods, to report when pairs of tasks are disjoint, and (ii) leveraging this information by introducing the SelectiveDisjunctive propagator which generates a lower bound on the earliest completion time of cliques of disjoint tasks to determine conflicts. This allows us to aggregate disjointness information spanning multiple constraints to gain a better global overview of the problem, as well as more precise local information. We also identify a problem structure where an LCG solver reasoning over Cumulative constraints separately, without any reformulations, requires an exponential amount of time to prove infeasibility, which we both justify theoretically and show empirically; on the other hand, our approach solves those instances in polynomial time. On particular known RCPSP and RCPSP/max benchmarks, our approach significantly reduces the number of conflicts required to prove optimality when resource contention is high. Additionally, we discover new lower bounds for 16 RCPSP/max instances (closing six of them) and four RCPSP instances (closing one), as well as new upper bounds for two RCPSP/max instances and four RCPSP instances. Furthermore, we empirically analyse our proposed approach to determine which features are beneficial for performance, showing that finding cliques is one of the main bottlenecks and that detecting disjointness during search can lead to improved bounds on certain instances, but it generally negatively impacts learning. This work paves the way for reasoning over the disjointness of tasks inferred from a variety of standard constraints to discover novel information sourced from multiple constraints during search.

Background: Modern SAT solvers are indispensable reasoning tools that are widely applied in verification, planning, and combinatorial design. Beyond answering satisfiability, they also produce unsatisfiability proofs, which are valuable for certification and analysis. Since there are no guarantees that their length is close to optimal, however, those proofs are insufficient to make claims about the gap between the solver proofs and the shortest possible proof. Understanding this gap is important for analyzing solver behavior, as it can be seen as a proxy for evaluating the room for improvement of the solver for the input formula in question. Objectives: We study the problem of finding the shortest resolution proofs for unsatisfiable formulas. Our goal is to understand how far solver-generated proofs deviate from the optimum, and to develop algorithms that can discover proofs substantially shorter than the solver-produced proofs. Methods: We propose a novel branch-and-bound algorithm for resolution proof length minimization. To facilitate it, we introduce a layer list representation that eliminates all symmetries from clause permutations, thereby improving upon an earlier SAT-encoding approach to proof length minimization. Further, we accelerate the search by integrating pruning techniques based on proof length lower bounds and clause subsumption. Results: Our algorithm consistently reduces solver proof lengths by 25–50% for synthetic instances and by 15—50% for formulas from the SAT Competition editions from 2002 to 2025, as well as halves the proof lengths for half of the available formulas from planning problems. As an exact method, it solves twice as many minimally unsatisfiable instances as the state-of-the-art approach and is faster by orders of magnitude on the overlapping instances. Conclusions: These results show that solver-generated proofs can often be substantially shortened—not by removing redundant claims, but by an entirely different chain of derivations—and that resolution proof length minimization is more tractable in practice than earlier approaches suggested. Our work highlights proof length minimization as a useful perspective for analyzing solver behavior and opens avenues for applying similar techniques to stronger proof systems.