Introduction to Constraint Solving

Author

Your Name

Published

February 5, 2025

Introduction

This lecture introduces the fundamental concepts of constraint solving, marking the beginning of our exploration into constraint programming. Our primary objective is to understand how to effectively model real-world problems as Constraint Satisfaction Problems (CSPs) and subsequently apply constraint programming techniques to derive solutions. This journey will encompass both the theoretical underpinnings and the practical applications of CSPs. We will begin by establishing a clear understanding of the core components of CSPs, including variables, domains, and constraints. Furthermore, we will delve into Constraint Optimization Problems (COPs), which extend the CSP framework by incorporating an objective function. Finally, we will discuss the historical and foundational role of SAT (Boolean Satisfiability) solvers in the evolution of modern constraint solving techniques, highlighting their significance in the field.

Constraint Satisfaction Problems (CSPs)

A Constraint Satisfaction Problem (CSP) is defined as a triple $P = (V, D, C)$, where:

$V = \{v_1, v_2, \dots, v_n\}$ is a finite set of variables. These variables represent the unknowns in the problem we are trying to solve.
$D = \{D_1, D_2, \dots, D_n\}$ is a set of domains. Each $D_i$ corresponds to a variable $v_i$ and specifies the set of possible values that $v_i$ can take.
$C = \{c_1, c_2, \dots, c_m\}$ is a set of constraints. Each constraint $c_i$ is a relation defined over a subset of the variables in $V$, specifying the allowed combinations of values for those variables.

Domains

Domains define the set of permissible values for each variable. These domains are typically finite, reflecting the practical nature of the problems we aim to model. For instance, in a graph coloring problem, the domain of each node might be a set of colors, such as {A, B, C} or {1, 2, 3}. The choice of domain representation does not affect the problem’s structure, as long as the number of values is finite.

Constraints

A constraint is a relation that restricts the simultaneous values that variables can assume. It embodies the problem’s rules and limitations.

Let $c \in C$ be a constraint involving variables $v_{i_1}, v_{i_2}, \dots, v_{i_k}$. Then $c$ is a relation defined on the Cartesian product of the domains of these variables: \[c \subseteq D_{i_1} \times D_{i_2} \times \dots \times D_{i_k}\] This means that $c$ is a set of tuples, where each tuple represents an allowed combination of values for the variables $v_{i_1}, v_{i_2}, \dots, v_{i_k}$.

Constraints can be expressed in various forms, including:

Unary relations: These involve a single variable, such as $x > 3$, which restricts the values that $x$ can take.
Binary relations: These involve two variables, such as $x \neq y$, which specifies that $x$ and $y$ cannot have the same value.
Higher-order relations: These involve three or more variables, such as $x + y + z < 10$, which restricts the sum of the values of $x$, $y$, and $z$.

Consider a constraint $c$ involving variables $x, y, z, t$. The constraint can be represented as a relation on the Cartesian product of their respective domains, $D_x \times D_y \times D_z \times D_t$. This relation specifies which combinations of values for $x, y, z,$ and $t$ are permitted according to the constraint $c$.

Solutions

A solution to a CSP is an assignment of values to all variables that satisfies all the constraints.

A solution to a CSP $P = (V, D, C)$ is an assignment $\sigma: V \to \bigcup_{i=1}^n D_i$ such that:

For each variable $v_i \in V$, the assigned value $\sigma(v_i)$ must be an element of the domain $D_i$. This ensures that the assignment respects the domain of each variable.
For each constraint $c \in C$ involving variables $v_{i_1}, \dots, v_{i_k}$, the tuple of assigned values $(\sigma(v_{i_1}), \dots, \sigma(v_{i_k}))$ must belong to the relation defined by $c$. This ensures that all constraints are satisfied by the assignment.

We denote the set of all solutions to a CSP $P$ as $\mathrm{sol}(P)$.

A CSP $P$ is said to be consistent or satisfiable if the set of solutions $\mathrm{sol}(P)$ is not empty (i.e., $\mathrm{sol}(P) \neq \emptyset$). This means that there exists at least one assignment of values to the variables that satisfies all the constraints. Otherwise, the CSP is said to be inconsistent or unsatisfiable, indicating that no such assignment exists.

Notation

To facilitate our discussion, we will use the following notation:

$\mathrm{sol}(P)$: Represents the set of all solutions of a CSP $P$.
$\mathrm{sol}(c)$: Represents the set of all solutions that satisfy a single constraint $c$.
$\mathrm{FV}(c)$ or $|c|$: Denotes the set of free variables (or the variables involved) in constraint $c$. The notation $\mathrm{FV}(c)$ is derived from first-order logic, where it represents the set of free variables in a formula.

Constraint Optimization Problems (COPs)

A Constraint Optimization Problem (COP) extends the framework of Constraint Satisfaction Problems (CSPs) by incorporating an objective function. This function allows us to not only find a solution that satisfies all constraints but also to find the "best" solution according to a defined criterion.

A Constraint Optimization Problem is defined as a CSP $P = (V, D, C)$ together with an objective function $f: D_1 \times D_2 \times \dots \times D_n \to \mathbb{R}$. The objective function $f$ maps each complete assignment of values to the variables (i.e., a tuple of values from the domains $D_1, D_2, \dots, D_n$) to a real number. The goal of a COP is to find a solution $\sigma \in \mathrm{sol}(P)$ that either minimizes or maximizes the value of the objective function $f(\sigma)$.

In essence, a COP seeks to find a solution that not only satisfies all the constraints of the problem but also optimizes a specific measure of the solution’s quality. This optimization can involve minimizing costs, maximizing profits, or achieving any other desired objective.

Example: Four Queens Problem

The Four Queens Problem is a classic example used to illustrate the concepts of Constraint Satisfaction Problems. The objective is to place four queens on a 4x4 chessboard such that no two queens threaten each other. This means no two queens can be in the same row, column, or diagonal.

Variables and Domains

Variables: We define four variables, $V = \{x_1, x_2, x_3, x_4\}$, where $x_i$ represents the row position of the queen in the $i$-th column. For example, $x_1 = 2$ indicates that the queen in the first column is placed in the second row.
Domains: Each variable $x_i$ has the same domain, $D_i = \{1, 2, 3, 4\}$, for all $i \in \{1, 2, 3, 4\}$. This means that each queen can be placed in any of the four rows.

Constraints

The constraints ensure that no two queens threaten each other. They can be divided into horizontal and diagonal constraints:

Horizontal constraints: No two queens can be in the same row. This is expressed as $x_i \neq x_j$ for all $1 \leq i < j \leq 4$. This constraint ensures that for any two columns $i$ and $j$, the queens must be placed in different rows.
Diagonal constraints: No two queens can be on the same diagonal. This is expressed as $|x_i - x_j| \neq |i - j|$ for all $1 \leq i < j \leq 4$. This constraint ensures that the absolute difference in row positions is not equal to the absolute difference in column positions for any two queens.

Horizontal Constraints as Relations

To illustrate how constraints can be represented as relations, let’s consider the horizontal constraint between $x_1$ and $x_2$, i.e., $x_1 \neq x_2$. This constraint can be explicitly represented as the following set of tuples: \[\{(1,2), (1,3), (1,4), (2,1), (2,3), (2,4), (3,1), (3,2), (3,4), (4,1), (4,2), (4,3)\}\] Each tuple $(a, b)$ in this set represents an allowed combination of values for $x_1$ and $x_2$, where $x_1 = a$ and $x_2 = b$. Note that tuples where $x_1 = x_2$ are excluded, as they violate the horizontal constraint.

Diagonal Constraints as Relations

Similarly, let’s consider the diagonal constraint between $x_1$ and $x_2$, i.e., $|x_1 - x_2| \neq |1 - 2|$, which simplifies to $|x_1 - x_2| \neq 1$. This constraint can be represented as: \[\{(1,1), (1,4), (2,1), (2,3), (3,2), (3,4), (4,1), (4,3), (4,4) \}\] The pairs $(1,3)$ and $(2,4)$ are excluded because $|1-3| = 2 = |1-2|$ and $|2-4| = 2 = |1-2|$, which violate the diagonal constraint. The pair $(1,2)$ is also excluded because $|1-2|=1$. Note that the tuple $(1,1)$ is allowed by the diagonal constraint, but it is not allowed by the horizontal constraint.

SAT: Satisfiability Problem

The Boolean Satisfiability Problem (SAT) is a fundamental problem in computer science and a specific instance of a Constraint Satisfaction Problem (CSP). In SAT, variables are restricted to Boolean values (0 or 1), and constraints are expressed as clauses in Conjunctive Normal Form (CNF).

Definition

Given a set of Boolean variables $X = \{x_1, x_2, \dots, x_n\}$ and a CNF formula $\phi = c_1 \wedge c_2 \wedge \dots \wedge c_m$, where each clause $c_i$ is a disjunction of literals (e.g., $x_1 \vee \neg x_2 \vee x_3$), the SAT problem is to find an assignment $\sigma: X \to \{0, 1\}$ such that $\phi$ is satisfied. A CNF formula is satisfied if each clause $c_i$ evaluates to 1 (true) under the assignment $\sigma$.

In simpler terms, the SAT problem asks whether there exists an assignment of true or false values to the variables in a given Boolean formula such that the entire formula evaluates to true. The formula is expressed in CNF, which is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals. A literal is either a variable or its negation.

Encoding SAT as CSP

A SAT problem can be directly encoded as a CSP, demonstrating that SAT is a specific type of CSP. The encoding is as follows:

Variables: The variables in the CSP are the same as the Boolean variables in the SAT problem, $X = \{x_1, x_2, \dots, x_n\}$.
Domains: The domain of each variable $x_i$ is $D_i = \{0, 1\}$, representing the Boolean values false (0) and true (1).
Constraints: Each clause $c_i$ in the CNF formula can be represented as a constraint. For example, the clause $x_1 \vee \neg x_2 \vee x_3$ can be represented as the constraint $x_1 + (1 - x_2) + x_3 \geq 1$. This constraint ensures that at least one literal in the clause is true (i.e., has a value of 1).

This encoding shows that solving a SAT problem is equivalent to solving a CSP with Boolean variables and constraints derived from the CNF formula.

Historical Context: DPLL Algorithm

The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a cornerstone in the field of automated reasoning and a foundational algorithm for solving SAT problems. Developed in the early 1960s, it combines deterministic constraint propagation with non-deterministic variable assignment, forming the basis for many modern SAT solvers and constraint programming techniques.

Key Ideas

The DPLL algorithm operates by systematically exploring the space of possible variable assignments. Its core ideas include:

Unit Propagation: This is a deterministic inference rule. If a clause contains only one unassigned literal and all other literals are false, then that unassigned literal must be set to true to satisfy the clause. This process is also known as Boolean Constraint Propagation (BCP).
Variable Selection and Assignment: When unit propagation can no longer deduce new assignments, the algorithm selects an unassigned variable and non-deterministically assigns it a value (either 0 or 1). This step introduces a branching point in the search space. The choice of which variable to assign and which value to try first can significantly impact the algorithm’s efficiency.
Backtracking: If an assignment leads to a conflict (i.e., a clause becomes false), the algorithm backtracks to the most recent branching point, undoes the assignment, and tries a different value for that variable. This is a depth-first search strategy.
Backjumping: This is an optimization over simple backtracking. When a conflict is encountered, backjumping analyzes the conflict to identify the variable assignments that caused the conflict. Instead of simply backtracking to the immediately preceding decision, it jumps back to the most recent decision that is relevant to the conflict, potentially skipping over irrelevant decision levels in the search tree. This is a more efficient way to explore the search space, avoiding unnecessary exploration of branches that are guaranteed to lead to a conflict.

Prop-Labeling Tree

The execution of the DPLL algorithm can be visualized as a search tree, often referred to as a prop-labeling tree. Each node in this tree represents a partial assignment of values to the variables, along with the results of constraint propagation. The tree is built by alternating between two main operations:

Prop (Propagation): Represents the deterministic constraint propagation phase. This corresponds to applying unit propagation (or BCP) to simplify the formula and deduce new assignments. This step is deterministic and does not involve any choices.
Labeling: Represents the non-deterministic variable assignment phase. This corresponds to selecting an unassigned variable and assigning it a value (either 0 or 1). This step introduces a branching point in the search tree.

The DPLL algorithm explores this tree in a depth-first manner, using backtracking (or backjumping) to recover from conflicts and explore alternative assignments.

Constraint Propagation

Constraint propagation is a crucial deterministic process in constraint solving. It aims to simplify a Constraint Satisfaction Problem (CSP) by reducing the search space without altering the set of solutions. This is achieved by inferring new constraints or reducing the domains of variables based on the existing constraints.

Definition

Constraint propagation is a procedure that transforms a CSP $P = (V, D, C)$ into another CSP $P' = (V, D', C')$ such that:

Solution Preservation: The set of solutions for the original CSP $P$ is the same as the set of solutions for the transformed CSP $P'$, i.e., $\mathrm{sol}(P) = \mathrm{sol}(P')$. This ensures that no solutions are lost during the transformation.
Simplification: The transformed CSP $P'$ is "simpler" than the original CSP $P$. This simplification can manifest in various ways, such as:
- Smaller Domains: The domains of some variables in $P'$ may be smaller than their corresponding domains in $P$. This means that some values that were previously possible for a variable are now known to be infeasible.
- Fewer Constraints: Some constraints in $P$ may be replaced by simpler or more explicit constraints in $P'$. This can make the problem easier to analyze and solve.

Constraint propagation is a deterministic process, meaning that it does not involve any non-deterministic choices or guessing. It uses logical inference to derive new information from the existing constraints and domains.

Example: Sudoku

A classic example of constraint propagation is seen in solving Sudoku puzzles. In Sudoku, the goal is to fill a 9x9 grid with digits from 1 to 9 such that each row, column, and 3x3 sub-grid contains all the digits from 1 to 9 without repetition.

If a cell is assigned a value (e.g., 2), constraint propagation removes the value 2 from the domains of all other cells in the same row, column, and 3x3 sub-grid.
This is because, according to the Sudoku rules, no two cells in the same row, column, or sub-grid can have the same value.
This process of removing values from domains based on existing assignments is an example of constraint propagation.

Complexity

Constraint propagation algorithms must be computationally efficient, typically running in polynomial time. This is because they are called repeatedly at each node of the search tree during the solution process. While constraint propagation can significantly reduce the search space, it cannot, in general, solve the CSP entirely on its own. The process of constraint propagation helps to reduce the complexity of the problem, making it easier for the search algorithm to find a solution.

Constraint propagation is a deterministic process that simplifies a CSP by reducing variable domains and inferring new constraints, while preserving the set of solutions. It is an essential component of constraint solvers, enabling them to efficiently explore the search space.

Conclusion

This lecture has provided a comprehensive introduction to the fundamental concepts of constraint solving. We began by defining Constraint Satisfaction Problems (CSPs), including their core components: variables, domains, and constraints. We then explored how solutions are defined within the CSP framework and discussed the concept of Constraint Optimization Problems (COPs), which extend CSPs by incorporating an objective function to be optimized. The Four Queens problem served as a practical example to illustrate these concepts, demonstrating how real-world problems can be modeled as CSPs. We also delved into the Boolean Satisfiability Problem (SAT) and its historical significance in the development of constraint solving techniques, particularly the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. A key takeaway from this lecture is the interplay between deterministic constraint propagation and non-deterministic variable assignment in solving CSPs. Constraint propagation simplifies the problem by reducing the search space, while variable assignment introduces branching points that are explored using backtracking or backjumping techniques.

Future Topics: In future lectures, we will delve deeper into the following topics:

Detailed analysis of constraint propagation algorithms: We will examine various constraint propagation techniques, including their implementation and complexity.
Strategies for variable selection and assignment: We will explore different heuristics for selecting variables and assigning values during the search process, aiming to improve the efficiency of constraint solvers.
Exploration of different types of constraints: We will investigate various types of constraints, including linear, quadratic, set constraints, and temporal constraints, and discuss how to handle them effectively.
Practical implementation of constraint solvers: We will discuss the practical aspects of building constraint solvers and the challenges involved in their implementation.
Improving the efficiency of constraint propagation: We will explore advanced techniques to enhance the performance of constraint propagation algorithms.
Strategies for variable selection in complex CSPs: We will examine sophisticated strategies for variable selection in complex CSPs to optimize the search process.

These future topics will build upon the foundational concepts introduced in this lecture, providing a deeper understanding of constraint solving and its applications.

--- title: "Introduction to Constraint Solving" author: "Your Name" date: "2025-02-05" format: html: toc: true # Table of Contents toc-depth: 2 code-tools: true theme: cosmo # Or "journal" for Distill-like minimalism --- # Introduction {#sec:introduction} This lecture introduces the fundamental concepts of constraint solving, marking the beginning of our exploration into constraint programming. Our primary objective is to understand how to effectively model real-world problems as Constraint Satisfaction Problems (CSPs) and subsequently apply constraint programming techniques to derive solutions. This journey will encompass both the theoretical underpinnings and the practical applications of CSPs. We will begin by establishing a clear understanding of the core components of CSPs, including variables, domains, and constraints. Furthermore, we will delve into Constraint Optimization Problems (COPs), which extend the CSP framework by incorporating an objective function. Finally, we will discuss the historical and foundational role of SAT (Boolean Satisfiability) solvers in the evolution of modern constraint solving techniques, highlighting their significance in the field. # Constraint Satisfaction Problems (CSPs) {#sec:csp} ::: tcolorbox []{#def:csp label="def:csp"} A Constraint Satisfaction Problem (CSP) is defined as a triple $P = (V, D, C)$, where: - $V = \{v_1, v_2, \dots, v_n\}$ is a finite set of variables. These variables represent the unknowns in the problem we are trying to solve. - $D = \{D_1, D_2, \dots, D_n\}$ is a set of domains. Each $D_i$ corresponds to a variable $v_i$ and specifies the set of possible values that $v_i$ can take. - $C = \{c_1, c_2, \dots, c_m\}$ is a set of constraints. Each constraint $c_i$ is a relation defined over a subset of the variables in $V$, specifying the allowed combinations of values for those variables. ::: ## Domains {#subsec:domains} Domains define the set of permissible values for each variable. These domains are typically finite, reflecting the practical nature of the problems we aim to model. For instance, in a graph coloring problem, the domain of each node might be a set of colors, such as {A, B, C} or {1, 2, 3}. The choice of domain representation does not affect the problem's structure, as long as the number of values is finite. ## Constraints {#subsec:constraints} A constraint is a relation that restricts the simultaneous values that variables can assume. It embodies the problem's rules and limitations. ::: tcolorbox []{#def:constraint label="def:constraint"} Let $c \in C$ be a constraint involving variables $v_{i_1}, v_{i_2}, \dots, v_{i_k}$. Then $c$ is a relation defined on the Cartesian product of the domains of these variables: $$c \subseteq D_{i_1} \times D_{i_2} \times \dots \times D_{i_k}$$ This means that $c$ is a set of tuples, where each tuple represents an allowed combination of values for the variables $v_{i_1}, v_{i_2}, \dots, v_{i_k}$. ::: Constraints can be expressed in various forms, including: - **Unary relations**: These involve a single variable, such as $x > 3$, which restricts the values that $x$ can take. - **Binary relations**: These involve two variables, such as $x \neq y$, which specifies that $x$ and $y$ cannot have the same value. - **Higher-order relations**: These involve three or more variables, such as $x + y + z < 10$, which restricts the sum of the values of $x$, $y$, and $z$. ::: tcolorbox []{#ex:constraint_example label="ex:constraint_example"} Consider a constraint $c$ involving variables $x, y, z, t$. The constraint can be represented as a relation on the Cartesian product of their respective domains, $D_x \times D_y \times D_z \times D_t$. This relation specifies which combinations of values for $x, y, z,$ and $t$ are permitted according to the constraint $c$. ::: ## Solutions {#subsec:solutions} A solution to a CSP is an assignment of values to all variables that satisfies all the constraints. ::: tcolorbox []{#def:solution_csp label="def:solution_csp"} A solution to a CSP $P = (V, D, C)$ is an assignment $\sigma: V \to \bigcup_{i=1}^n D_i$ such that: 1. For each variable $v_i \in V$, the assigned value $\sigma(v_i)$ must be an element of the domain $D_i$. This ensures that the assignment respects the domain of each variable. 2. For each constraint $c \in C$ involving variables $v_{i_1}, \dots, v_{i_k}$, the tuple of assigned values $(\sigma(v_{i_1}), \dots, \sigma(v_{i_k}))$ must belong to the relation defined by $c$. This ensures that all constraints are satisfied by the assignment. ::: We denote the set of all solutions to a CSP $P$ as $\mathrm{sol}(P)$. ::: tcolorbox []{#def:consistency label="def:consistency"} A CSP $P$ is said to be **consistent** or **satisfiable** if the set of solutions $\mathrm{sol}(P)$ is not empty (i.e., $\mathrm{sol}(P) \neq \emptyset$). This means that there exists at least one assignment of values to the variables that satisfies all the constraints. Otherwise, the CSP is said to be **inconsistent** or **unsatisfiable**, indicating that no such assignment exists. ::: ## Notation {#subsec:notation} To facilitate our discussion, we will use the following notation: - $\mathrm{sol}(P)$: Represents the set of all solutions of a CSP $P$. - $\mathrm{sol}(c)$: Represents the set of all solutions that satisfy a single constraint $c$. - $\mathrm{FV}(c)$ or $|c|$: Denotes the set of free variables (or the variables involved) in constraint $c$. The notation $\mathrm{FV}(c)$ is derived from first-order logic, where it represents the set of free variables in a formula. # Constraint Optimization Problems (COPs) {#sec:cop} A Constraint Optimization Problem (COP) extends the framework of Constraint Satisfaction Problems (CSPs) by incorporating an objective function. This function allows us to not only find a solution that satisfies all constraints but also to find the \"best\" solution according to a defined criterion. ::: tcolorbox []{#def:cop label="def:cop"} A Constraint Optimization Problem is defined as a CSP $P = (V, D, C)$ together with an objective function $f: D_1 \times D_2 \times \dots \times D_n \to \mathbb{R}$. The objective function $f$ maps each complete assignment of values to the variables (i.e., a tuple of values from the domains $D_1, D_2, \dots, D_n$) to a real number. The goal of a COP is to find a solution $\sigma \in \mathrm{sol}(P)$ that either minimizes or maximizes the value of the objective function $f(\sigma)$. ::: In essence, a COP seeks to find a solution that not only satisfies all the constraints of the problem but also optimizes a specific measure of the solution's quality. This optimization can involve minimizing costs, maximizing profits, or achieving any other desired objective. # Example: Four Queens Problem {#sec:four_queens} The Four Queens Problem is a classic example used to illustrate the concepts of Constraint Satisfaction Problems. The objective is to place four queens on a 4x4 chessboard such that no two queens threaten each other. This means no two queens can be in the same row, column, or diagonal. ## Variables and Domains {#subsec:four_queens_vars_domains} - **Variables**: We define four variables, $V = \{x_1, x_2, x_3, x_4\}$, where $x_i$ represents the row position of the queen in the $i$-th column. For example, $x_1 = 2$ indicates that the queen in the first column is placed in the second row. - **Domains**: Each variable $x_i$ has the same domain, $D_i = \{1, 2, 3, 4\}$, for all $i \in \{1, 2, 3, 4\}$. This means that each queen can be placed in any of the four rows. ## Constraints {#subsec:four_queens_constraints} The constraints ensure that no two queens threaten each other. They can be divided into horizontal and diagonal constraints: - **Horizontal constraints**: No two queens can be in the same row. This is expressed as $x_i \neq x_j$ for all $1 \leq i < j \leq 4$. This constraint ensures that for any two columns $i$ and $j$, the queens must be placed in different rows. - **Diagonal constraints**: No two queens can be on the same diagonal. This is expressed as $|x_i - x_j| \neq |i - j|$ for all $1 \leq i < j \leq 4$. This constraint ensures that the absolute difference in row positions is not equal to the absolute difference in column positions for any two queens. ### Horizontal Constraints as Relations {#subsubsec:horizontal_relations} To illustrate how constraints can be represented as relations, let's consider the horizontal constraint between $x_1$ and $x_2$, i.e., $x_1 \neq x_2$. This constraint can be explicitly represented as the following set of tuples: $$\{(1,2), (1,3), (1,4), (2,1), (2,3), (2,4), (3,1), (3,2), (3,4), (4,1), (4,2), (4,3)\}$$ Each tuple $(a, b)$ in this set represents an allowed combination of values for $x_1$ and $x_2$, where $x_1 = a$ and $x_2 = b$. Note that tuples where $x_1 = x_2$ are excluded, as they violate the horizontal constraint. ### Diagonal Constraints as Relations {#subsubsec:diagonal_relations} Similarly, let's consider the diagonal constraint between $x_1$ and $x_2$, i.e., $|x_1 - x_2| \neq |1 - 2|$, which simplifies to $|x_1 - x_2| \neq 1$. This constraint can be represented as: $$\{(1,1), (1,4), (2,1), (2,3), (3,2), (3,4), (4,1), (4,3), (4,4) \}$$ The pairs $(1,3)$ and $(2,4)$ are excluded because $|1-3| = 2 = |1-2|$ and $|2-4| = 2 = |1-2|$, which violate the diagonal constraint. The pair $(1,2)$ is also excluded because $|1-2|=1$. Note that the tuple $(1,1)$ is allowed by the diagonal constraint, but it is not allowed by the horizontal constraint. # SAT: Satisfiability Problem {#sec:sat} The Boolean Satisfiability Problem (SAT) is a fundamental problem in computer science and a specific instance of a Constraint Satisfaction Problem (CSP). In SAT, variables are restricted to Boolean values (0 or 1), and constraints are expressed as clauses in Conjunctive Normal Form (CNF). ## Definition {#subsec:sat_definition} ::: tcolorbox []{#def:sat_problem label="def:sat_problem"} Given a set of Boolean variables $X = \{x_1, x_2, \dots, x_n\}$ and a CNF formula $\phi = c_1 \wedge c_2 \wedge \dots \wedge c_m$, where each clause $c_i$ is a disjunction of literals (e.g., $x_1 \vee \neg x_2 \vee x_3$), the SAT problem is to find an assignment $\sigma: X \to \{0, 1\}$ such that $\phi$ is satisfied. A CNF formula is satisfied if each clause $c_i$ evaluates to 1 (true) under the assignment $\sigma$. ::: In simpler terms, the SAT problem asks whether there exists an assignment of true or false values to the variables in a given Boolean formula such that the entire formula evaluates to true. The formula is expressed in CNF, which is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals. A literal is either a variable or its negation. ## Encoding SAT as CSP {#subsec:sat_as_csp} A SAT problem can be directly encoded as a CSP, demonstrating that SAT is a specific type of CSP. The encoding is as follows: - **Variables**: The variables in the CSP are the same as the Boolean variables in the SAT problem, $X = \{x_1, x_2, \dots, x_n\}$. - **Domains**: The domain of each variable $x_i$ is $D_i = \{0, 1\}$, representing the Boolean values false (0) and true (1). - **Constraints**: Each clause $c_i$ in the CNF formula can be represented as a constraint. For example, the clause $x_1 \vee \neg x_2 \vee x_3$ can be represented as the constraint $x_1 + (1 - x_2) + x_3 \geq 1$. This constraint ensures that at least one literal in the clause is true (i.e., has a value of 1). This encoding shows that solving a SAT problem is equivalent to solving a CSP with Boolean variables and constraints derived from the CNF formula. # Historical Context: DPLL Algorithm {#sec:dpll} The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a cornerstone in the field of automated reasoning and a foundational algorithm for solving SAT problems. Developed in the early 1960s, it combines deterministic constraint propagation with non-deterministic variable assignment, forming the basis for many modern SAT solvers and constraint programming techniques. ## Key Ideas {#subsec:dpll_key_ideas} The DPLL algorithm operates by systematically exploring the space of possible variable assignments. Its core ideas include: - **Unit Propagation**: This is a deterministic inference rule. If a clause contains only one unassigned literal and all other literals are false, then that unassigned literal must be set to true to satisfy the clause. This process is also known as Boolean Constraint Propagation (BCP). - **Variable Selection and Assignment**: When unit propagation can no longer deduce new assignments, the algorithm selects an unassigned variable and non-deterministically assigns it a value (either 0 or 1). This step introduces a branching point in the search space. The choice of which variable to assign and which value to try first can significantly impact the algorithm's efficiency. - **Backtracking**: If an assignment leads to a conflict (i.e., a clause becomes false), the algorithm backtracks to the most recent branching point, undoes the assignment, and tries a different value for that variable. This is a depth-first search strategy. - **Backjumping**: This is an optimization over simple backtracking. When a conflict is encountered, backjumping analyzes the conflict to identify the variable assignments that caused the conflict. Instead of simply backtracking to the immediately preceding decision, it jumps back to the most recent decision that is relevant to the conflict, potentially skipping over irrelevant decision levels in the search tree. This is a more efficient way to explore the search space, avoiding unnecessary exploration of branches that are guaranteed to lead to a conflict. ## Prop-Labeling Tree {#subsec:prop_labeling_tree} The execution of the DPLL algorithm can be visualized as a search tree, often referred to as a prop-labeling tree. Each node in this tree represents a partial assignment of values to the variables, along with the results of constraint propagation. The tree is built by alternating between two main operations: - **Prop (Propagation)**: Represents the deterministic constraint propagation phase. This corresponds to applying unit propagation (or BCP) to simplify the formula and deduce new assignments. This step is deterministic and does not involve any choices. - **Labeling**: Represents the non-deterministic variable assignment phase. This corresponds to selecting an unassigned variable and assigning it a value (either 0 or 1). This step introduces a branching point in the search tree. The DPLL algorithm explores this tree in a depth-first manner, using backtracking (or backjumping) to recover from conflicts and explore alternative assignments. # Constraint Propagation {#sec:constraint_propagation} Constraint propagation is a crucial deterministic process in constraint solving. It aims to simplify a Constraint Satisfaction Problem (CSP) by reducing the search space without altering the set of solutions. This is achieved by inferring new constraints or reducing the domains of variables based on the existing constraints. ## Definition {#subsec:cp_definition} ::: tcolorbox []{#def:constraint_propagation label="def:constraint_propagation"} Constraint propagation is a procedure that transforms a CSP $P = (V, D, C)$ into another CSP $P' = (V, D', C')$ such that: 1. **Solution Preservation**: The set of solutions for the original CSP $P$ is the same as the set of solutions for the transformed CSP $P'$, i.e., $\mathrm{sol}(P) = \mathrm{sol}(P')$. This ensures that no solutions are lost during the transformation. 2. **Simplification**: The transformed CSP $P'$ is \"simpler\" than the original CSP $P$. This simplification can manifest in various ways, such as: - **Smaller Domains**: The domains of some variables in $P'$ may be smaller than their corresponding domains in $P$. This means that some values that were previously possible for a variable are now known to be infeasible. - **Fewer Constraints**: Some constraints in $P$ may be replaced by simpler or more explicit constraints in $P'$. This can make the problem easier to analyze and solve. ::: Constraint propagation is a deterministic process, meaning that it does not involve any non-deterministic choices or guessing. It uses logical inference to derive new information from the existing constraints and domains. ## Example: Sudoku {#subsec:cp_sudoku_example} A classic example of constraint propagation is seen in solving Sudoku puzzles. In Sudoku, the goal is to fill a 9x9 grid with digits from 1 to 9 such that each row, column, and 3x3 sub-grid contains all the digits from 1 to 9 without repetition. - If a cell is assigned a value (e.g., 2), constraint propagation removes the value 2 from the domains of all other cells in the same row, column, and 3x3 sub-grid. - This is because, according to the Sudoku rules, no two cells in the same row, column, or sub-grid can have the same value. - This process of removing values from domains based on existing assignments is an example of constraint propagation. ## Complexity {#subsec:cp_complexity} Constraint propagation algorithms must be computationally efficient, typically running in polynomial time. This is because they are called repeatedly at each node of the search tree during the solution process. While constraint propagation can significantly reduce the search space, it cannot, in general, solve the CSP entirely on its own. The process of constraint propagation helps to reduce the complexity of the problem, making it easier for the search algorithm to find a solution. ::: tcolorbox Constraint propagation is a deterministic process that simplifies a CSP by reducing variable domains and inferring new constraints, while preserving the set of solutions. It is an essential component of constraint solvers, enabling them to efficiently explore the search space. ::: # Conclusion {#sec:conclusion} This lecture has provided a comprehensive introduction to the fundamental concepts of constraint solving. We began by defining Constraint Satisfaction Problems (CSPs), including their core components: variables, domains, and constraints. We then explored how solutions are defined within the CSP framework and discussed the concept of Constraint Optimization Problems (COPs), which extend CSPs by incorporating an objective function to be optimized. The Four Queens problem served as a practical example to illustrate these concepts, demonstrating how real-world problems can be modeled as CSPs. We also delved into the Boolean Satisfiability Problem (SAT) and its historical significance in the development of constraint solving techniques, particularly the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. A key takeaway from this lecture is the interplay between deterministic constraint propagation and non-deterministic variable assignment in solving CSPs. Constraint propagation simplifies the problem by reducing the search space, while variable assignment introduces branching points that are explored using backtracking or backjumping techniques. **Future Topics:** []{#subsec:future_topics label="subsec:future_topics"} In future lectures, we will delve deeper into the following topics: - **Detailed analysis of constraint propagation algorithms**: We will examine various constraint propagation techniques, including their implementation and complexity. - **Strategies for variable selection and assignment**: We will explore different heuristics for selecting variables and assigning values during the search process, aiming to improve the efficiency of constraint solvers. - **Exploration of different types of constraints**: We will investigate various types of constraints, including linear, quadratic, set constraints, and temporal constraints, and discuss how to handle them effectively. - **Practical implementation of constraint solvers**: We will discuss the practical aspects of building constraint solvers and the challenges involved in their implementation. - **Improving the efficiency of constraint propagation**: We will explore advanced techniques to enhance the performance of constraint propagation algorithms. - **Strategies for variable selection in complex CSPs**: We will examine sophisticated strategies for variable selection in complex CSPs to optimize the search process. These future topics will build upon the foundational concepts introduced in this lecture, providing a deeper understanding of constraint solving and its applications.