Encoding single-constant multiplication (SCM) constraints into SAT is essential for solving a wide range of combinatorial problems involving integer arithmetic. Although optimal SAT encodings for SCM are known, they are often prohibitively expensive to generate for large constants. This paper introduces a dynamic programming (DP) approach that offers a practical balance between encoding quality and encoding time. The proposed method recursively decomposes the binary representation of the target constant into chunks and eliminates common subexpressions across the chunks and their one's complements. The objective is either to minimize the number of additions (the min-k objective) or to minimize the number of half/full adders (the min-a objective). The DP algorithm is naturally expressed and efficiently implemented using mode-directed tabling in Picat. Although the approach does not guarantee optimality, experimental results show that it produces high-quality encodings while substantially reducing encoding time.

Traditionally, SAT encodings of complex constraints, such as linear constraints or more specifically PB constraints, are specified in terms of Boolean variables and clauses. However, often sets of related Boolean variables are either encodings of integer variables, or act as if they were. Furthermore, any encoding of linear constraints has to encode partial sums, and these are integers (even if the encoding does not explicitly notice this). By formally specifying the SAT encoding using integer variables and constraints, coupled with a procedure to encode this specification into SAT, we can gain some more insight into the encoding methods, and compose new ones. Experiments using these integer-driven encodings show that they can improve on standard approaches to encoding PB and integer linear constraints to SAT.

In this paper we focus on a challenging version of the aircraft maintenance routing problem (AMRP) with a maintenance distribution objective (AMRP-D). For the AMRP-D, the flight legs with predefined start and end times are assigned to aircraft. In addition to the assigned flight legs, each aircraft has to satisfy certain regulations regarding the maintenance services that are mandatory in the scheduling period, while the maintenance should also be distributed evenly. We propose a two stage approach, where first we use a decomposition method that is solved using constraint programming, to cover the flight legs. To optimize the distribution objective, we propose two metaheuristic techniques based on Large Neighborhood Search (LNS) and Simulated Annealing (SA). The LNS method consists of different destroy operators and as repairer we use a constraint programming (CP) solver. The SA approach includes a novel neighborhood to deal with the distribution objective. Our experimental results show that the decomposition method is able to solve more instances than the exact approach, while SA provides better quality solutions for the optimization stage compared to LNS.

Recent pseudo-Boolean (PB) solvers leverage the cutting planes proof system to perform SAT-style conflict analysis during search. This process learns implied PB constraints, which can prune later parts of the search tree and is crucial to a PB solver's performance. A key step in PB conflict analysis is the reduction of a reason constraint, which caused a variable propagation that contributed to the conflict. While necessary, reduction generally makes the reason constraint less strong. Consequently, different approaches to reduction have been proposed, broadly categorised as division- or saturation-based, with the aim of preserving the strength of the reason constraint as much as possible. This paper proposes two novel techniques in each reduction category. We theoretically show how each technique yields reason constraints which are at least as strong as those obtained from existing reduction methods. We then evaluate the empirical effectiveness of the reduction techniques on hard knapsack instances and the most recent PB'24 competition benchmarks.

The aircraft maintenance routing problem with a maintenance distribution objective (AMRP-D) considers a set of flight legs that have to be assigned to a set of available aircraft. While the start and end time of the flight legs are specified in advance, the aircraft are required to undergo various maintenance tasks in the planning horizon. Scheduling these maintenance tasks as evenly as possible is the objective of the AMRP-D, however, for most instances it is even difficult to find a feasible solution covering all maintenance requirements. This paper presents a new constraint programming model for the stated problem in order to provide feasible solutions for small instances. The proposed model is tested on the available benchmark instances, resulting in more feasible solutions.

This paper presents new methods of encoding the multiplication of a binary encoded integer variable with a constant value for Boolean Satisfiability (SAT) solvers. This problem, known as the Single Constant Multiplication (SCM) problem, is widely studied for its application in hardware design, but this technique are currently not employed for SAT encodings. Considering the smaller and variable bit sizes and the different cost of operations in SAT, we propose further improvements to existing methods by minimising the number of full/half adders, rather than the number of ripple carry adders. We compare our methods to simple encodings into adders, currently employed by SAT encoders, and direct Boolean encoding using logic minimisation tools. We show that our methods result in improved solve-time for problems involving integer linear constraints. A library of optimal recipes for each method to encode SCM for SAT is made available as part of this publication.

Combinatorial Optimization (CO) is the mathematical study of decision-making problems, which occur throughout nature and society. Examples of CO problems span a wide range of fields, including logistics (e.g. workforce rostering, vehicle routing), information technology (e.g. network routing, software compilation, hardware verification), ethics (e.g. resource allocation, voting audits), gaming (e.g. pathfinding), and so on. Often, engineers face two types of challenges when tackling CO problems. On the one hand, the problem's textbook definition does not cover the real-world complexities with its ever-changing requirements and infinite details. On the other hand, the computational hardness of even the textbook definition dictates that there currently is no known algorithm to solve it efficiently - and there likely never will be.

Constraint Programming (CP) is a programming paradigm which separates these two concerns. It allows the user to mathematically specify the real-world complexities in a constraint model. The model is then solved by powerful solvers. A translation layer between model and solver ensures that changes in the details of the problem only require changes in the model, but not in the solver.

This thesis studies the translation (or encoding) of models to a particular type of solver based on Boolean Satisfiability (SAT). The performance of these SAT solvers has dramatically improved in the last twenty years, standing out in solver competitions and industrial use cases. However, encoding a constraint model into SAT is uniquely difficult. Usually, multiple encodings of the same problem are possible, and one can be far more easy to solve than another, and there is no straightforward way to predict which is best.

Boolean satisfiability (SAT) solvers have dramatically improved their performance in the last twenty years, enabling them to solve large and complex problems. More recently MaxSAT solvers have appeared that efficiently solve optimisation problems based on SAT. This means that SAT solvers have become a competitive technology for tackling discrete optimisation problems. A challenge in using SAT solvers for discrete optimisation is the many choices of encoding a problem into SAT. When encoding integer variables appearing in discrete optimisation problems, SAT must choose an encoding for each variable. Typical approaches fix a common encoding for all variables. However, different constraints are much more effective when encoded with a particular encoding choice. This inevitably leads to models where variables have different variable encodings. These models must then be able to couple encodings, either by using multiple encoding of single variables and channelling between the representations, or by encoding constraints using a mix of representations for the variables involved. In this paper we show how using mixed encodings of integers and coupled encodings of constraints can lead to better (Max)SAT models of discrete optimisation problems.

Combinatorial (optimization) problems occur in nature and society. Constraint modeling languages such as MiniZinc allow the user to declaratively specify such problems in terms of its decision variables and constraints. Subsequently, the MiniZinc model can be compiled into an equivalent (Boolean) SAT formula to be solved by a SAT solver. This thesis reports on the design, implementation and experimental evaluation of the new MiniZinc-SAT compiler, which supports single or even mixed usage of three distinct integer variable encoding methods.