Sudoku and Satisfiability Modulo Theories

Introduction

Imagine you’re trying to solve a puzzle where you have to figure out whether certain statements can all be true at the same time. This might sound simple, but what if those statements involve complex rules and relationships? Problems like these are at the heart of SAT (Boolean Satisfiability Problem) and SMT (Satisfiability Modulo Theories), two important topics in computer science and logic. They help us solve complex puzzles in many areas, from designing computer chips to scheduling tasks. This essay will explore what SAT and SMT are, why they matter, and how they are used in real-world situations.

As a fun and practical example of how these tools can be used, we’ll end this post by showing how SMT can be used to solve Sudoku puzzles, turning a well-known puzzle into a logic-based problem-solving task.

SAT

SAT stands for Boolean Satisfiability Problem. It’s all about answering a basic question: “Can we assign True or False values to certain variables in a way that makes a given logical formula true?”

Think of SAT as a logic puzzle. Here’s an example:

You’re given the statements:

1. x or y (meaning one of them, or both, must be True).

2. Not x or z (meaning either x is False, or z is True, or both).

3. Not y or not z (meaning at least one of y or z must be False).

Can you assign True or False values to x, y, and z that make all of these statements true at the same time?

This is a SAT problem! The goal is to find a solution where the statements don’t contradict each other, or determine if no such solution exists.

Propositional logic

Propositional logic, also known as Boolean logic, deals with statements that can either be True or False. These statements are called propositions, and they are combined using logical operators to form propositional logic formulas.

A proposition is a statement that has a definite truth value—either True or False. For example:

• “It is raining” is a proposition, and it can be either True or False.

• In mathematical terms, we often use variables to represent propositions. For example, we might let:

  • x represent “It is raining”.

  • y represent “It is cloudy”.

Each of these variables can take the value True or False.

In propositional logic, we use logical operators to combine propositions into more complex formulas. The most important operators are:

• AND ( ∧ ): The expression x \land y is True only if both x and y are True. Example: “It is raining and it is cloudy” is only True if both things are happening.

• OR ( ∨ ): The expression x \lor y is True if either x or y (or both) are True. Example: “It is raining or it is cloudy” is True if at least one of them is happening.

• NOT ( ¬ ): The expression \neg x (read as “not x”) is True if x is False. Example: “It is not raining” is True if x is False (i.e., it is not raining).

• Implication ( → ): The expression x \rightarrow y (read as “if x, then y”) is True unless x is True and y is False. Example: “If it is raining, then it is cloudy” is True unless it’s raining but not cloudy.

A propositional logic formula is a combination of variables and logical operators that can be evaluated as True or False, depending on the values of the variables.

For example, consider the formula:

(x \lor y) \land (\neg x \lor z)

This formula combines the variables x, y, and z using the logical operators AND, OR, and NOT. The task is to determine whether there are values for x, y, and z that make the whole formula True. This is exactly what the SAT problem asks us to solve.

Decision problems

A decision problem is a question that can be answered with a simple Yes or No. In the case of SAT, the decision problem is:

“Given a propositional logic formula, is there an assignment of True/False values to the variables that makes the formula True?”

If such an assignment exists, the answer is Yes, and we say the formula is satisfiable. If no such assignment exists, the answer is No, and we say the formula is unsatisfiable.

Let’s consider a simple SAT problem:

(x \lor y) \land (\neg x \lor z) \land (\neg y \lor \neg z)

We want to know if there’s a way to assign True or False values to x, y, and z so that the entire formula is True.

Let’s try a few combinations:

• If x = \mathrm{True}, y = \mathrm{True}, z = \mathrm{True}: (x \lor y) is \mathrm{True}, (\neg x \lor z) is \mathrm{True}, but (\neg y \lor \neg z) is \mathrm{False}. This assignment does not satisfy the formula.

• If x = \mathrm{True}, y = \mathrm{False}, z = \mathrm{True}: (x \lor y) is \mathrm{True}, (\neg x \lor z) is \mathrm{True}, and (\neg y \lor \neg z) is \mathrm{True}. This assignment does satisfy the formula!

So, the formula is satisfiable, and the answer to the SAT problem is Yes.

Standardizing SAT problems

Many SAT problems are written in a special format called Conjunctive Normal Form (CNF). A formula is in CNF if it is a conjunction (AND) of one or more clauses, where each clause is a disjunction (OR) of literals. A literal is simply a variable or its negation.

For example, the formula:

(x \lor \neg y) \land (\neg x \lor z \lor y)

is in CNF because it is an AND of two OR clauses.

Why is CNF important? SAT solvers (programs designed to solve SAT problems) work more efficiently when the formula is in CNF. In fact, any propositional logic formula can be converted into CNF without changing its satisfiability.

NP-complete problems

SAT is the first problem ever proven to be NP-complete. This means that:

1. SAT is in NP: Given a solution (an assignment of True/False values), we can check if it satisfies the formula in a reasonable amount of time (in polynomial time).

2. SAT is NP-hard: Every problem in NP can be reduced to SAT in polynomial time. In simpler terms, if we can solve SAT quickly, we can solve every problem in NP quickly.

This discovery has huge implications in computer science because it shows how SAT is connected to many other difficult problems. If we can find an efficient algorithm to solve SAT, we can apply it to a wide range of important problems, like optimization, scheduling, and even cryptography.

SAT solvers: how do they work?

SAT problems can get very complicated, especially when there are many variables and clauses. To solve them efficiently, we use SAT solvers, which are computer programs designed to find solutions to SAT problems. SAT solvers use several smart strategies to speed up the search for a solution. Two of the most common strategies are:

• Backtracking: The solver tries different assignments of True/False values, and if it hits a dead end (an unsatisfiable assignment), it backtracks and tries a different path.

• Unit propagation: If a clause contains only one unassigned variable, the solver can immediately assign it a value that satisfies the clause.

Modern SAT solvers can solve problems with thousands or even millions of variables and clauses. These solvers are used in many applications, including verifying that hardware circuits work correctly and solving complex puzzles like Sudoku.

Real-world applications

Now that we know what SAT is, let’s explore some real-world uses:

• Hardware and software verification: Before building a computer chip, engineers use SAT to check that the design behaves correctly. A mistake in the design could cause a computer to crash or malfunction. SAT solvers help catch these errors before they become costly problems. Similarly, SAT is used in software verification to ensure that a program behaves as expected under all possible conditions.

• AI and decision making: In artificial intelligence (AI), SAT is used to solve planning and decision-making problems. For example, SAT can help an AI system figure out the best sequence of actions to achieve a goal while following certain rules.

• Puzzles and games: Many logic-based puzzles, like Sudoku or Minesweeper, can be turned into SAT problems. A SAT solver can then be used to find the solution to the puzzle, or to check if the puzzle has a unique solution.

SMT

Now that we have a solid understanding of SAT and how it helps us solve problems using propositional logic (True/False values), let’s take things a step further with SMT, or Satisfiability Modulo Theories. While SAT focuses only on whether a logical formula can be true or false, SMT opens the door to solving more complex mathematical problems that involve numbers, functions, arrays, and even more abstract concepts. SMT combines the power of SAT with other theories from mathematics to tackle a wider range of problems.

Like SAT, SMT asks whether a certain formula can be made True, but it doesn’t limit itself to just logical variables (True/False values). Instead, SMT allows us to work with mathematical objects like:

• Integers (whole numbers).

• Real numbers (including fractions and decimals).

• Arrays (lists of elements).

• Functions (mathematical relationships).

With SMT, we can ask questions that involve not just logic but also arithmetic, like: “Is there a way to assign values to x and y such that x + y = 5 and x > 2?”

In this case, x and y are not just True or False; they are numbers. SMT solvers, just like SAT solvers, try to find values for the variables that satisfy all the given conditions.

Theories

In SMT, the word theory refers to a set of rules that describe how certain kinds of mathematical objects behave. These theories help the SMT solver understand and solve problems that go beyond simple logic. Let’s take a look at some common theories used in SMT:

• Linear arithmetic: This theory deals with equations and inequalities involving numbers. It allows us to solve problems like:

  • x + y = 10.

  • 3x - 2y \leq 5.

  • x \geq 0.

The SMT solver uses the rules of arithmetic to find values for x and y that satisfy these equations.

• Bit-vectors: Bit-vectors represent numbers in binary form (0s and 1s), which is how computers store and manipulate data. Bit-vector theory is important in verifying how computer hardware (like circuits) works. For example:

  • x \& y = 1.

  • x \text{ shifted left by } 2 = z.

  These operations are common in low-level computing tasks, and SMT solvers can handle them by using the rules of bit-wise operations.

• Arrays and functions: Arrays are lists of numbers or objects, and functions describe how inputs are mapped to outputs. SMT solvers can reason about arrays and functions using logical and mathematical rules. For example, in array theory, you might ask: “Is there a way to assign values to an array such that the sum of all its elements is 20?”, or in function theory: “Is there a function f(x) that satisfies f(2) = 4 and f(3) = 9?”.

How SMT solvers work

SMT solvers work in two main steps:

1. Boolean abstraction: The solver first treats the problem as a SAT problem by working with the Boolean logic part. It temporarily ignores the complicated mathematical parts (like numbers or arrays) and focuses on the logical structure.

2. Theory solving: After the SAT part is solved, the SMT solver checks if the numbers, arrays, or functions meet the additional constraints defined by the theory. If the SAT part leads to a solution that violates the mathematical rules (e.g., if the solution says x + y = 10 but the theory says that’s not possible), the solver tries a different assignment.

This combination of logical reasoning (like in SAT) and mathematical reasoning (using theories) makes SMT solvers extremely powerful.

Complexity

SMT is NP-hard, meaning it is at least as hard as the hardest problems in NP. This is important because many real-world problems can be formulated as SMT problems, and solving them efficiently is difficult. Like SAT, SMT involves searching through many possible assignments for variables, but in addition to simple logic, the solver must also deal with more complex mathematical theories (such as arithmetic or arrays).

This makes SMT harder to solve than pure SAT problems because the solver not only needs to find a logical assignment but also ensure that it satisfies the rules of the mathematical theory involved. Despite this complexity, SMT solvers have become incredibly advanced and are used in many real-world applications.

Why SMT is powerful

While SAT is a powerful tool for solving logical problems that involve only True/False values, SMT goes much further. It combines logic with mathematics, allowing us to solve more complex problems that involve not just logical variables, but also numbers, functions, arrays, and other mathematical structures. By incorporating theories such as arithmetic, arrays, and functions, SMT enables us to reason about problems that SAT alone cannot handle.

In a SAT problem, we are limited to determining whether a set of logical conditions can all be true at once, with variables that can only be True or False. While this is useful in many areas (like circuit verification and puzzle-solving), it doesn’t account for problems that involve numbers, functions, or more abstract data types.

SMT enhances SAT by allowing us to work with variables that take on more complex values and obey specific rules (or theories). This means that SMT can handle problems like:

• Arithmetic: Finding numbers that satisfy equations or inequalities.

• Bit-vectors: Verifying computer hardware by modeling numbers as binary digits.

• Arrays: Working with data structures, such as lists or tables, and reasoning about how elements are stored and accessed.

• Functions: Handling relationships between inputs and outputs, which is useful for reasoning about computer programs or mathematical models.

For example, consider a problem where you need to find two numbers, x and y, such that:

• x + y = 10.

• x > 3.

• y \leq 6.

A simple SAT solver cannot deal with this because it only works with True/False values. An SMT solver, however, can use linear arithmetic theory to find values for x and y that satisfy these conditions.

Real-world applications

Because SMT solvers can handle both logic and mathematics, they are used in a wide range of real-world applications. These applications often involve problems where both logical conditions and numerical relationships must be satisfied at the same time. Here are a few important areas where SMT solvers play a critical role:

• Verifying computer programs: In the world of software, programs are expected to behave correctly no matter what inputs they receive or what paths their execution follows. SMT solvers are used to formally verify that programs do not crash, run into errors, or behave unexpectedly.

  For instance, if you write a program that calculates the square root of a number, you need to make sure it never tries to compute the square root of a negative number (which would cause an error). An SMT solver can check all possible inputs to ensure that the program handles every situation correctly, even the edge cases that a human might miss.

  By using SMT, software engineers can catch potential bugs before they happen, preventing costly errors in industries like aerospace, medical devices, or financial systems, where software correctness is absolutely critical.

• Solving scheduling problems: SMT solvers are also used in scheduling—a problem that involves assigning tasks to people, machines, or time slots while following certain rules. These rules might include constraints like:

  • A task can only start after another task is finished.

  • Some tasks cannot be done at the same time.

  • Certain workers are only available at specific times.

  Imagine trying to schedule a series of construction tasks on a large building site. Each task depends on other tasks being completed (you can’t install the windows before the walls are built!), and you only have a limited number of workers available. SMT solvers can process these constraints and find an optimal schedule that minimizes delays and uses resources efficiently.

  This ability to handle both logical dependencies and numerical constraints makes SMT invaluable for resource allocation, project planning, and logistics in industries like manufacturing, transportation, and healthcare.

• Optimizing circuit designs: In hardware design, particularly for computer chips, engineers need to ensure that the circuit behaves correctly under all possible input combinations. This is critical because even a small error can lead to catastrophic consequences, like a computer crashing or malfunctioning. Using bit-vector theory, SMT solvers model how circuits manipulate binary data (0s and 1s) and check whether the circuit design meets the required specifications. For example, SMT can verify that:

  • A chip correctly adds two numbers without overflow.

  • A processor handles all operations within its performance constraints.

  In addition, SMT solvers can optimize designs by ensuring that the chip uses the least amount of resources (such as power or space) while still functioning correctly. This makes them indispensable in the semiconductor industry, where efficient design is key to building faster, smaller, and more energy-efficient devices.

Efficiency and scalability of SMT solvers

SMT solvers are designed to handle highly complex problems, often involving thousands or even millions of variables and constraints. This capability to scale and manage complexity efficiently is one of the key reasons why SMT solvers have become indispensable in many fields. Unlike simpler solvers that can only handle basic logical formulas, modern SMT solvers—such as Z3 (developed by Microsoft)—can work on incredibly large and intricate problems that require the integration of both logic and mathematics.

Large-Scale software verification

Software verification is a critical application of SMT solvers. Large and complex codebases, like those used in operating systems or flight control software, require guarantees that they behave correctly in every possible situation. This is especially important for safety-critical systems, where even a small bug could lead to catastrophic consequences (such as an airplane malfunctioning or a medical device failing). SMT solvers are used to automatically verify that a program adheres to its specifications by checking all possible inputs and paths the software might take.

For example, verifying that a piece of software does not crash when it processes certain inputs might require checking billions of different combinations of inputs and internal states. An SMT solver can analyze these possibilities using logical and mathematical models, ensuring that the software behaves as expected across all cases. This process, known as formal verification, is a step beyond typical software testing because it proves the absence of errors rather than simply checking for errors that are found during testing.

Optimizing systems

Another area where SMT solvers excel is system optimization. Many real-world systems—such as networks, electronic circuits, or transportation schedules—are incredibly complex, involving a large number of interacting components that must work together efficiently. SMT solvers help optimize these systems by finding the best possible configuration that meets all the necessary constraints.

For instance, in network design, you might need to ensure that data flows through the network as efficiently as possible while minimizing costs and avoiding congestion. SMT solvers can handle the complexity of these requirements, modeling both the logical rules that govern the network’s behavior and the mathematical constraints, such as bandwidth limits or latency requirements.

In circuit design, SMT solvers are used to minimize the power consumption, size, and heat production of electronic circuits while ensuring they perform their intended functions correctly. As circuits become more advanced and compact, this optimization process becomes critical for the performance of modern electronics, including smartphones and computer processors.

In large-scale scheduling problems—such as assigning shifts to employees or scheduling jobs on machines—SMT solvers help find optimal solutions that balance competing demands, such as time constraints, available resources, and efficiency goals. Because SMT solvers can scale to handle thousands of tasks or constraints, they are a powerful tool for solving these optimization problems in real-world industrial settings.

Advanced techniques

Even though SMT is NP-hard, meaning that, in the worst cases, solving these problems can take an enormous amount of time—the development of advanced algorithms and heuristics has made SMT solvers much faster and more practical for real-world applications. SMT solvers use several techniques to reduce the time and resources required to find a solution, including:

• Backtracking: The solver explores possible solutions and, if it hits a dead end (where a solution doesn’t work), it backtracks to an earlier decision point and tries a different path. This helps the solver avoid wasting time on unworkable solutions.

• Conflict-Driven Clause Learning (CDCL): When the solver encounters a conflict (a situation where no solution can satisfy the current set of constraints), it learns from this conflict to avoid making similar mistakes in the future. This dramatically speeds up the solving process by preventing the solver from revisiting paths that are known to be dead ends.

• Theory Propagation: Theories in SMT (such as arithmetic or arrays) have their own specific rules. SMT solvers use theory propagation to narrow down the possible values for variables based on the rules of these theories. For example, if a variable must satisfy a certain arithmetic equation, the solver can limit the range of possible values for that variable, which reduces the complexity of the search.

By combining these techniques, SMT solvers are able to handle problems that would be intractable for simpler solvers, allowing them to efficiently solve highly complex and large-scale problems.

Combining multiple theories

One of the key strengths of SMT solvers is their ability to handle multiple theories simultaneously, allowing them to solve problems that involve not just simple logic but a mixture of complex mathematical domains. This combination of theories allows SMT solvers to model real-world systems with a higher degree of accuracy and sophistication. By integrating diverse theories, SMT solvers can solve problems that span multiple domains of mathematics and logic in a seamless way. Let’s take a closer look at how multiple theories work together in SMT, and why this makes SMT solvers exceptionally powerful.

When we talk about SMT solvers “combining multiple theories,” what we really mean is that the solver is capable of reasoning about different kinds of constraints that apply to different types of data—all at the same time.

Each theory brings its own set of rules and constraints. For example:

• Arithmetic theory deals with equations and inequalities.

• Array theory includes operations like indexing and updating.

• Bit-vector theory includes binary manipulations like bit-shifting or bitwise AND/OR operations.

In real-world applications, it’s rare for a problem to belong to just one theory. Often, multiple theories are at play. SMT solvers shine in such scenarios by integrating these different theories and coordinating the solving process so that constraints from all applicable theories are satisfied simultaneously.

Let’s now explore some concrete examples where multiple theories interact in SMT.

Verifying software with mixed data types

Consider a software verification problem in which a program performs both arithmetic computations and manipulates arrays. Suppose the program performs operations like:

1. Arithmetic: x = a + b.

2. Array access: Reading an element from an array arr[i].

3. Bitwise operations: z = x \& y, where \& is the bitwise AND operation.

To ensure the correctness of this program, we need to check if the program will behave correctly for any given inputs. Here’s how multiple theories would be combined by the SMT solver:

1. Arithmetic theory will handle the equation x = a + b, ensuring that the sum is computed correctly according to arithmetic rules. The solver will also check that variables like x, a, and b are appropriately constrained (e.g., x must be an integer).

2. Array theory will handle the operation arr[i], ensuring that the index i is valid (i.e., it lies within the bounds of the array). It will also ensure that the right value is retrieved from the array and assigned to the right variable. The solver checks that accessing arr[i] doesn’t lead to an out-of-bounds error.

3. Bit-vector theory will manage the bitwise operation z = x \& y, ensuring that the binary representation of x and y is correctly manipulated at the bit level. This is crucial for many low-level computing tasks, such as encoding or encryption, where binary data is processed.

By combining these theories, the SMT solver verifies that the program will execute correctly, no matter what values are assigned to the variables. The solver considers all possible inputs and execution paths to prove that there are no runtime errors, incorrect calculations, or invalid memory accesses.

A coordinated process

The magic of SMT solvers lies in their ability to coordinate between these multiple theories while solving a problem. Theories often interact in complex ways, so SMT solvers must communicate between theories to resolve constraints effectively. This involves a process known as theory combination or theory propagation.

1. Theory propagation: Each theory can propagate constraints based on its specific rules. For example, if the arithmetic theory deduces that x > 10, then this information is passed to the array theory to check if accessing arr[x] is still valid, ensuring x doesn’t exceed the array bounds.

2. Conflict resolution: If a conflict arises—such as the arithmetic theory concluding x = 5, while the bit-vector theory requires x to have a binary value that would make x = 3, the solver identifies this conflict and attempts to resolve it by exploring alternative solutions. This iterative process is essential for finding a solution that satisfies all constraints across different theories.

3. Theory interpolation: When two different theories interact, SMT solvers use techniques like theory interpolation to reconcile their different views of the problem. For instance, arithmetic may dictate that x = 4, while array theory may require that x be within certain index limits. The solver navigates these competing constraints by narrowing down possible values for x that satisfy both theories.

These interactions make SMT solvers more efficient at solving problems that would be too difficult for simpler solvers that only handle one theory at a time.

Flexibility across domains

The flexibility of SMT solvers to combine multiple theories makes them incredibly versatile. Here are a few real-world examples that highlight their power across different domains:

• Cryptographic verification: SMT solvers are used to verify cryptographic algorithms, such as those used for data encryption and digital signatures. Cryptographic operations often involve both arithmetic (modular arithmetic over large numbers) and bitwise manipulations (such as shifting bits or performing XOR operations).

  For instance, verifying the correctness of a RSA encryption algorithm requires an SMT solver to:

  • Check the modular arithmetic involved in key generation and encryption.

  • Ensure the bitwise operations used to encode and decode messages are performed correctly.

  By integrating arithmetic and bit-vector theories, an SMT solver can ensure that the algorithm is mathematically secure and functions as expected for all inputs.

• Optimizing robotic movements: In modern factories, robots are often programmed to perform complex tasks that involve both decision-making (logic) and precise control of movement (arithmetic). SMT solvers are used to optimize robotic movements, ensuring that they follow the most efficient path while respecting physical constraints like speed, distance, and safety.

  An SMT solver may combine:

  • Linear arithmetic to model the robot’s physical movements.

  • Logic to represent decision-making rules, such as “if an obstacle is detected, stop the robot.”

  • Array theory to manage data about the robot’s environment and task status.

  By solving these constraints together, the SMT solver finds an optimal plan for the robot that minimizes movement time, avoids obstacles, and completes tasks in the most efficient way possible.

• Artificial Intelligence: Planning and Scheduling: AI systems often need to make decisions that involve both logic and time-based scheduling. For example, an AI planning system might need to schedule tasks for multiple robots working in parallel, ensuring that each robot finishes its task without clashing with others.

  SMT solvers can:

  • Use arithmetic theory to track time constraints, such as ensuring that task A is completed before task B starts.

  • Use array theory to keep track of which robot is performing which task.

  • Use logical reasoning to decide the best sequence of actions.

  By combining these theories, SMT solvers can efficiently plan out the most effective way for robots to complete tasks without delays or conflicts, making AI systems smarter and more reliable.

Z3

Z3¹ is one of the most widely-used and powerful SMT solvers, developed by Microsoft Research. It is designed to solve logical and mathematical problems that involve both Boolean logic (True/False values) and a variety of mathematical structures, such as integers, real numbers, arrays, bit-vectors, and more. Z3 has become the go-to tool for a wide range of applications, from verifying software correctness to optimizing systems in industrial engineering. Its ability to handle large and complex problems efficiently, while combining different mathematical theories, sets it apart from other solvers.

¹ de Moura, L., & Bjørner, N. (2008). Z3: An Efficient SMT Solver. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Link to paper

Key features:

• Multi-theory solver: Z3 can handle problems that involve multiple theories simultaneously, such as arithmetic, bit-vectors, arrays, and functions. This makes it versatile enough to solve complex real-world problems that span multiple domains of logic and mathematics. Whether you are working with numerical constraints, manipulating data structures like arrays, or verifying hardware circuits that operate at the bit level, Z3 can manage these interactions seamlessly.

• High efficiency: Z3 is designed to solve extremely large problems with millions of variables and constraints. It employs advanced techniques, such as conflict-driven clause learning (CDCL), backtracking, and theory propagation, to explore the search space efficiently. These techniques enable Z3 to quickly find solutions or prove that no solution exists, even for problems that are computationally intensive.

• Combining logical and mathematical constraints: One of Z3’s most powerful features is its ability to combine logical constraints (such as those used in SAT solving) with mathematical constraints (such as equations and inequalities). For example, in software verification, Z3 can check both the logical flow of the program and the correctness of its arithmetic operations, ensuring that a program behaves as expected in all possible scenarios.

• Modularity and extensibility: Z3 is highly modular, which means that users can extend its capabilities to suit specific applications. It allows developers to define custom theories and tailor the solver’s behavior to fit the particular needs of their problem domain. This flexibility makes Z3 suitable for a wide range of industries, including aerospace, finance, cybersecurity, and hardware design.

• Rich API support: Z3 provides rich API support for various programming languages, including Python, C++, and Java. This means that users can integrate Z3 into their existing software tools and workflows easily. For instance, developers can use Z3 within a Python environment to model complex optimization problems, check for software bugs, or verify hardware designs. Its user-friendly interface and robust API make Z3 accessible to both researchers and engineers.

• Proving and model generation: In addition to solving for satisfiability, Z3 can also be used to prove the correctness of formulas or generate models that demonstrate specific properties. For example, in verifying a software system, Z3 can either provide a counterexample where the program fails or prove that no such failure exists under any circumstances. This capability is essential in formal methods for software and hardware verification.

API basic usage

The Z3 solver API provides a powerful interface for solving constraint satisfaction problems in Python. To use it, you first need to import Z3’s key components, such as Solver(), Int(), and constraint functions like And(), Or(), and Distinct().

You start by defining variables using Int() for integers or other types like Bool() for Boolean values. For example, to define an integer variable X and Y, you can do:

from z3 import Int


X = Int('X')
Y = Int('Y')

This creates two integer variables X and Y that can take integer values.

Next, you initialize the Z3 solver using the Solver() class. The solver will handle adding constraints and finding solutions. For example:

from z3 import Solver


1solver = Solver()

1

Initialize the Z3 solver.

Now, you can add constraints to the solver using solver.add(). For example, let’s say you want to add a constraint that the sum of X and Y should equal 10, and both X and Y should be greater than 0:

from z3 import Solver


1solver.add(X + Y == 10)
2solver.add(X > 0, Y > 0)

1

Add constraint that X + Y equals 10.

2

Add constraint that X and Y are greater than 0.

You can also use logical operators like Or() and And() for more complex constraints. For example:

1from z3 import Int, Solver, Or, And


2X = Int('X')
3Y = Int('Y')

4solver = Solver()

5solver.add(X + Y == 10)

6solver.add(And(X > 0, Y > 0))

7solver.add(Or(X < 5, Y > 5))

1

Import Z3 components: Int for integer variables, Solver to set up the constraint solver, and Or and And for logical operations.

2

Define an integer variable X using Z3’s Int constructor.

3

Define another integer variable Y.

4

Initialize the solver.

5

Add constraint: X + Y == 10, so the sum of X and Y must equal 10.

6

Add constraint using And(): Both X and Y must be greater than 0.

7

Add constraint using Or(): Either X is less than 5 or Y is greater than 5.

Once all constraints are added, you check whether the solver can find a solution by calling solver.check():

1if solver.check() == sat:
2  model = solver.model()

3  print(f"X = {model.evaluate(X)}")
  print(f"Y = {model.evaluate(Y)}")

else:
    print("No solution found")

1

Call to solver.check() causes the execution of the actual constraint-solving algorithm. If solver.check() returns sat, then it means Z3 found a solution.

2

solver.model() retrieves the solution.

3

model.evaluate(X) retrieves the value of the variable X from the solution (model) that Z3 has already found after executing the full algorithm during the solver.check() call.

The solver.check() method is used to determine whether the given set of constraints is satisfiable. The result of solver.check() can be one of three possible values:

• sat (satisfiable): This means that Z3 has found at least one solution that satisfies all the constraints you’ve provided. If solver.check() == sat, it means that Z3 was able to find a solution where all the constraints hold true.

• unsat (unsatisfiable): This means that there is no possible solution that satisfies the given set of constraints. If solver.check() returns unsat, it means that the constraints are contradictory, and Z3 cannot find any values for the variables that satisfy all the constraints.

• unknown: This means Z3 could not determine whether the constraints are satisfiable or unsatisfiable, often due to the complexity of the problem or limitations in the solver’s ability to handle the specific problem. This result can happen in more complex cases, such as problems involving non-linear arithmetic or other advanced features.

Here’s a complete example that ties everything together:

1from z3 import Int, Solver, Or, And, sat


2X = Int('X')
3Y = Int('Y')

4solver = Solver()

5solver.add(X + Y == 10)

6solver.add(And(X > 0, Y > 0))

7solver.add(Or(X < 5, Y > 5))

8if solver.check() == sat:
9  model = solver.model()

10  print(f"Solution: X = {model.evaluate(X)}, Y = {model.evaluate(Y)}")

else:
11  print("No solution found")

1

Import Z3 components: Int for integer variables, Solver to set up the constraint solver, and Or and And for logical operations.

2

Define an integer variable X using Z3’s Int constructor.

3

Define another integer variable Y.

4

Initialize the solver.

5

Add constraint: X + Y == 10, so the sum of X and Y must equal 10.

6

Add constraint using And(): Both X and Y must be greater than 0.

7

Add constraint using Or(): Either X is less than 5 or Y is greater than 5.

8

Check if the constraints are satisfiable.

9

Retrieve the solution model if satisfiable.

10

Print the values of X and Y. Output: Solution: X = 4, Y = 6.

11

Print a message if no solution is found.

This simple example shows how Z3 can be used in Python to solve constraint satisfaction problems. With just a few lines of code, you can define variables, add constraints, and let Z3 find solutions for you. This makes Z3 a powerful tool for solving puzzles, optimization problems, or more complex logical tasks.

API overview

The Z3 solver API provides a robust framework for solving a wide range of problems, including logic, optimization, and constraint satisfaction, using SMT (Satisfiability Modulo Theories). It leverages mathematical methods such as Boolean satisfiability (SAT), linear arithmetic, and theory solvers (for arrays, bit-vectors, real arithmetic, etc.). Z3’s API allows you to formulate complex problems in terms of constraints and logical propositions, which it then solves using advanced heuristics, backtracking, and conflict-driven clause learning (CDCL).

Overview of Z3 API concepts:

• Z3 supports different types of variables, such as:

  • Integers (Int()).

  • Booleans (Bool()).

  • Real numbers (Real()).

  • Bit-vectors (BitVec()).

  Each variable is associated with a domain, and constraints are imposed on these variables. For instance:

  from z3 import Int, Bool
  
  X = Int('X')  # Integer variable
  B = Bool('B')  # Boolean variable

• Z3 allows you to add arithmetic, logical, and set-theoretic constraints to your problem. These constraints can involve:

  • Arithmetic operations: +, -, *, /.

  • Logical operations: And(), Or(), Not(), Implies().

  • Relational operations: <, >, ==, !=.

  • Set operations: Distinct() (for ensuring distinct values in a set of variables).

  Example:

  1from z3 import Int, Solver, And, Or, Not, Distinct, sat
  
  
  2X = Int('X')
  3Y = Int('Y')
  4Z = Int('Z')
  
  5solver = Solver()
  
  6solver.add(X + 2 * Y == 10)
  
  7solver.add(And(X > 0, Y < 10))
  
  8solver.add(Z > X, Y < Z)
  
  9solver.add(Distinct(X, Y, Z))
  
  10if solver.check() == sat:
  11  model = solver.model()
  
  12  print(f"Solution: X = {model.evaluate(X)}, Y = {model.evaluate(Y)}, Z = {model.evaluate(Z)}")
  
  else:
  13  print("No solution found")
  

  1

  Import the necessary components: Z3 components such as Int, Solver, And, Distinct, etc., are imported.

  2

  Define an integer variable X using Z3’s Int constructor.
  

  3

  Define another integer variable Y.

  4

  Define a third integer variable Z.

  5

  Set up the Z3 solver: This initializes the solver that will manage and solve the constraints.

  6

  Add an arithmetic constraint: X + 2 * Y == 10 ensures that X plus twice Y equals 10.

  7

  Add a logical constraint: X > 0 and Y < 10 using the And() function.
  

  8

  Add relational constraints: Z > X and Y < Z to ensure relations between X, Y, and Z.
  

  9

  Add distinctness constraint: Distinct(X, Y, Z) ensures that X, Y, and Z all have distinct values.
  

  10

  Check if the constraints are satisfiable using solver.check().
  

  11

  Retrieve the model (solution) if the constraints are satisfiable.
  

  12

  Print the solution for X, Y, and Z. Output: Solution: X = 10, Y = 0, Z = 11.

  13

  Print a message if no solution is found.

• Z3 excels in combining SAT solvers with theory solvers for specific domains. Theories are specialized solvers that handle specific classes of constraints:

  • Linear arithmetic: Handles constraints involving addition, subtraction, and multiplication by constants (e.g., X + Y >= 10).

  • Non-linear arithmetic: Handles more complex polynomial expressions.

  • Bit-vectors: Useful for hardware modeling, where operations are performed on fixed-size binary numbers (e.g., BitVec('X', 32) for a 32-bit integer).

  • Arrays and functions: Z3 supports reasoning about arrays and functions, allowing for the definition of array indices and function applications.

• Z3 works by converting the problem into a Boolean satisfiability (SAT) problem and then applying conflict-driven clause learning (CDCL) to explore possible solutions. It divides the problem into Boolean logic and theory-specific reasoning (such as arithmetic or bit-vector theory). The general solving process involves:

  • SAT-based search: Z3 uses efficient SAT-solving techniques to find assignments to variables.

  • Theory propagation: Z3 incorporates theory solvers to check consistency within a specific theory (e.g., arithmetic or arrays).

  • Backtracking and learning: If a contradiction is encountered, Z3 backtracks and uses the learned conflict to prune the search space, improving efficiency.

• Z3 also supports optimization over variables, where you can minimize or maximize a given objective function. This is useful in cases where you are not just looking for any solution, but the best one (e.g., minimal cost, maximum profit). You can use Optimize() instead of Solver() to define an optimization problem:

  1from z3 import Int, Optimize, sat
  
  
  2X = Int('X')
  3Y = Int('Y')
  
  4opt = Optimize()
  
  5opt.add(X + Y >= 10)
  
  6opt.minimize(X)
  
  7if opt.check() == sat:
  8  model = opt.model()
  
  9  print(f"Solution: X = {model.evaluate(X)}, Y = {model.evaluate(Y)}")
  
  else:
  10  print("No solution found")
  

  1

  Import the necessary components: We import Int to define integer variables and Optimize for optimization.
  

  2

  Define an integer variable X using Z3’s Int constructor.
  

  3

  Define another integer variable Y.
  

  4

  Initialize the Z3 optimizer: Instead of using Solver(), we use Optimize() to allow the solver to minimize or maximize values.

  5

  Add a constraint: The sum of X + Y must be greater than or equal to 10.
  

  6

  Minimize X: We tell Z3 to minimize the value of X.
  

  7

  Check if the problem is satisfiable: Z3 checks if it can satisfy the constraints while optimizing.
  

  8

  Retrieve the model (solution) if the problem is satisfiable.
  

  9

  Print the solution for X and Y. Output: Solution: X = 10, Y = 0.

  10

  Print a message if no solution is found.

• Advanced solver techniques:

  • Conflict-driven clause learning (CDCL): Z3 uses CDCL to handle the SAT problem. It systematically explores possible assignments and learns from conflicts (inconsistent assignments) to avoid repeating them.

  • Backjumping and restarting: Z3 employs heuristics that help it decide when to backtrack, restart, or jump past certain unsolvable branches to explore more promising parts of the search space.

  • Theory combination: Z3 excels at combining different theories. For example, you can solve problems that simultaneously involve linear arithmetic, arrays, and bit-vectors, combining results from theory solvers to find the overall solution.

• Z3 supports first-order logic and can handle universal and existential quantifiers. You can express statements like “for all” or “there exists” using ForAll() and Exists(), respectively. The example given below will demonstrate the use of both universal and existential quantifiers. We’ll check if the solver can find a value for Y that satisfies a certain property for all values of X (universal quantification), and whether there exists a value of X that satisfies a condition (existential quantification).

  1from z3 import Int, Solver, ForAll, Exists, Implies, Or, And, sat
  
  
  2X = Int('X')
  3Y = Int('Y')
  
  4solver = Solver()
  
  5domain = [1, 2, 3]
  
  6solver.add(ForAll([X], Implies(Or([X == val for val in domain]), X + Y >= 5)))
  
  7solver.add(Exists([X], And(Or([X == val for val in domain]), X + Y == 6)))
  
  8if solver.check() == sat:
  9  model = solver.model()
  
  10  print(f"Solution: Y = {model.evaluate(Y)}")
  
  else:
  11  print("No solution found")
  

  1

  Import required Z3 components: Int, Solver, ForAll, Exists, Implies, Or, and And.
  

  2

  Define an integer variable X using Z3’s Int constructor.
  

  3

  Define another integer variable Y.

  4

  Initialize the Z3 solver using the Solver() class to manage and solve constraints.

  5

  Define the finite domain of X as [1, 2, 3].
  

  6

  Add a universal quantifier constraint: For all X in the domain, X + Y >= 5.
  

  7

  Add an existential quantifier constraint: There exists an X in the domain such that X + Y == 6.
  

  8

  Check if the constraints are satisfiable using solver.check().
  

  9

  Retrieve the model (solution) if the constraints are satisfiable.
  

  10

  Print the value of Y from the model (solution). Output: Solution: Y = 4.

  11

  Print a message if no solution is found.

• Z3 can generate proofs for unsatisfiable queries, showing why no solution exists for a given set of constraints. This is useful for formal verification tasks where you need to prove the correctness of systems, such as verifying hardware circuits or ensuring software correctness.

• Mathematical methods:

  • SAT Solvers: Z3 primarily uses Boolean satisfiability solvers, which handle the basic logic of whether a problem can be satisfied given the constraints. Z3 applies CDCL techniques to improve efficiency in solving SAT problems.

  • Theory Solvers:

    • Linear arithmetic solvers: These handle systems of linear inequalities and equations.

    • Non-linear arithmetic solvers: For handling polynomial constraints.

    • Bit-vector theory: This theory is used to model and verify properties of hardware systems where operations are performed on fixed-length bit-vectors.

    • Array theory: Provides reasoning about operations on arrays, such as read and write operations, making Z3 suitable for reasoning about data structures and memory models.

  • Optimization algorithms: Z3’s Optimize() module uses linear programming and mixed-integer programming techniques to find solutions that optimize an objective function under a set of constraints.

  • Quantifier elimination: Z3 implements methods for handling quantifiers in first-order logic, allowing it to reason about quantified statements efficiently.

Complete example

1from z3 import Int, Solver, And, Or, sat


2X = Int('X')
3Y = Int('Y')

4solver = Solver()

5solver.add(X + Y == 10)
6solver.add(And(X > 0, Y > 0))
7solver.add(Or(X == 3, Y == 7))

8if solver.check() == sat:
9  model = solver.model()
  
10  print(f"Solution: X = {model.evaluate(X)}, Y = {model.evaluate(Y)}")

else:
11  print("No solution found")

1

Import the required Z3 components: Int, Solver, And, Or, and sat.

2

Define an integer variable X using Z3’s Int constructor.

3

Define another integer variable Y.

4

Set up the Z3 solver using the Solver() class to manage and solve constraints.

5

Add an arithmetic constraint: X + Y must equal 10.

6

Add a logical constraint: Both X and Y must be greater than 0.

7

Add a logical disjunction: Either X is equal to 3, or Y is equal to 7.

8

Check if the constraints are satisfiable using solver.check().

9

Retrieve the model (solution) if the constraints are satisfiable.

10

Print the values of X and Y from the model (solution). Output: Solution: X = 3, Y = 7.

11

Print a message if no solution is found.

Uninterpreted functions

Uninterpreted functions in Z3 allow you to work with symbolic functions without specifying their exact definition or behavior. They are useful in scenarios where you want to reason about relationships between variables without providing the actual function’s implementation. Z3 treats these functions symbolically, meaning you only impose constraints on the inputs and outputs rather than defining the internal workings of the function.

Uninterpreted functions are commonly used in formal verification (e.g., verifying the correctness of algorithms or systems), theory reasoning, and model checking, where you care about the relationships between function calls but not necessarily their specific behavior.

In Z3, you can define an uninterpreted function using Function() and specify the domain and range of the function. You can then impose constraints on how the function behaves for certain inputs and reason about its properties.

Suppose we have a function f(x) which maps integers to integers. We don’t know the exact behavior of f(x), but we want to reason about its properties—specifically, we want to know if f(x) satisfies certain conditions.

Here’s how you define and work with an uninterpreted function in Z3:

1from z3 import Int, Function, Solver, IntSort, sat


2x = Int('x')
3y = Int('y')

4f = Function('f', IntSort(), IntSort())

5solver = Solver()

6solver.add(f(x) == y + 2)
7solver.add(f(3) == 5)
8solver.add(f(4) == 6)
9solver.add(f(7) == 10)

10if solver.check() == sat:
11  model = solver.model()
  
12  print(f"Solution: f(x) = {model.evaluate(f(x))}, y = {model.evaluate(y)}")
13  print(f"f(3) = {model.evaluate(f(3))}, f(4) = {model.evaluate(f(4))}, f(7) = {model.evaluate(f(7))}")
  
else:
14  print("No solution found")

1

Import required components from the Z3 solver library.

2

Define integer variable x.

3

Define integer variable y.

4

Define an uninterpreted function f that takes an integer and returns an integer.

5

Set up the solver by initializing an instance of the Solver() class.

6

Add a constraint specifying that f(x) is equal to y + 2.

7

Add a constraint specifying that f(3) must equal 5.

8

Add a constraint specifying that f(4) must equal 6.

9

Add a constraint specifying that f(7) must equal 10.

10

Check if the constraints are satisfiable.

11

Retrieve the model (solution) if the constraints are satisfiable.

12

Print the solution for f(x) and y. Output: Solution: f(x) = 5, y = 3.

13

Print the solution for f(3), f(4), and f(7). Output: f(3) = 5, f(4) = 6, f(7) = 10.

14

Print a message if no solution is found.

If the solver finds a solution, you will see something like:

Solution: f(x) = 5, y = 3
f(3) = 5, f(4) = 6, f(7) = 10

This shows that f(3), f(4), and f(7) satisfy the imposed constraints, while f(x) is defined symbolically as y + 2 for an arbitrary x.

Use cases for uninterpreted functions:

• Abstract Reasoning: Uninterpreted functions allow you to reason abstractly about the behavior of functions without specifying their exact definitions.

• Formal verification: In program verification, you can model abstract operations or methods as uninterpreted functions and reason about their effects on program state.

• Theorem proving: They can be used in automated theorem proving, where certain properties of functions are inferred based on logical constraints.

Sudoku time!

Intro

Sudoku is a logic-based number placement puzzle that can be played on grids of various sizes. The goal is to fill the grid such that each row, each column, and each subgrid contains a complete set of numbers without any repetition.

Sudoku puzzles can be played on any n \times n grid, where n is the square of an integer (e.g., 4, 9, 16). For example, in a 4 \times 4 Sudoku, you fill the grid with the numbers 1 to 4, in a 9 \times 9 Sudoku (the standard version), you fill the grid with the numbers 1 to 9, and so on.

General Sudoku rules:

1. Each row must contain a complete set of numbers from 1 to n, without repetition.

2. Each column must contain a complete set of numbers from 1 to n, without repetition.

3. Each subgrid (which is typically a \sqrt{n} \times \sqrt{n} box) must also contain a complete set of numbers from 1 to n, without repetition.

Grid sizes:

• Mini Sudoku: This is a smaller version with 4 \times 4 grid, ideal for beginners. The subgrids are 2 \times 2, and the puzzle uses digits 1 to 4.

• Standard Sudoku: This is the most common version, with 9 \times 9 grid, 3 \times 3 subgrids and digits 1 to 9.

• Large Sudoku: This uses larger grids, 16 \times 16 grid, 4 \times 4 subgrids, and digits 1 to 16.

• Extreme Sudoku: Rarely seen, this massive 25 \times 25 grid uses 5 \times 5 subgrids and digits 1 to 25, and is extremely challenging.

The difficulty of a Sudoku puzzle depends on several factors:

• Number of pre-filled cells: Easier puzzles have more numbers pre-filled, leaving fewer cells to solve. Harder puzzles have fewer pre-filled cells, requiring more deduction and logic.

• Type of logical strategies required:

  • Easy puzzles: Can often be solved using basic strategies like scanning rows, columns, and subgrids for obvious placements.

  • Medium puzzles: May require more advanced techniques like naked pairs or hidden pairs (where two cells in a row, column, or subgrid must contain specific numbers).

  • Hard puzzles: Often involve techniques like X-Wing, Swordfish, or backtracking where trial and error may be needed to determine the correct number.

  • Extreme puzzles: In extreme cases, solving may require highly complex strategies and involve much deeper logical deductions.

Let’s start playing

Here is the Python code for solving a Sudoku 9 \times 9 puzzle² using Z3, including a function that takes the puzzle as input and returns the solved puzzle, along with a main function that demonstrates its use.

² In the world of standard 9 \times 9 Sudoku puzzles, one of the most fascinating mathematical discoveries is the 17-Clue Theorem. In 2012, researchers Gary McGuire, Bastian Tugemann, and Gilles Civario proved through exhaustive computation that 17 is the minimum number of clues required for a standard 9 \times 9 Sudoku puzzle to have a unique solution. See McGuire, G., Tugemann, B., & Civario, G. (2014). There Is No 16-Clue Sudoku: Solving the Sudoku Minimum Number of Clues Problem via Hitting Set Enumeration. Experimental Mathematics, 23(2), 190–217. DOI

Let’s solve the following:

5	3	0	0	7	0	0	0	0
6	0	0	1	9	5	0	0	0
0	9	8	0	0	0	0	6	0
8	0	0	0	6	0	0	0	3
4	0	0	8	0	3	0	0	1
7	0	0	0	2	0	0	0	6
0	6	0	0	0	0	2	8	0
0	0	0	4	1	9	0	0	5
0	0	0	0	8	0	0	7	9

Code that leverages Z3 is:

1from z3 import Int, Solver, And, Distinct, sat


# Function to check if the solved Sudoku is correct
def is_valid_sudoku(solution):
  # Combined row and column checks in a single loop
  for i in range(9):
    # Check distinct values in row
    if len(set(solution[i])) != 9:  
2      return False
    
    # Check distinct values in column
    col = [solution[j][i] for j in range(9)]

    if len(set(col)) != 9:
3      return False

  # Check 3x3 subgrids
  for i in range(0, 9, 3):
    for j in range(0, 9, 3):
      subgrid = [solution[i + di][j + dj] for di in range(3) for dj in range(3)]

      if len(set(subgrid)) != 9:
4        return False

5  return True

def solve_sudoku(puzzle):
6  X = [[Int(f"x_{i}_{j}") for j in range(9)] for i in range(9)]
  
7  solver = Solver()
  
8  solver.add([And(X[i][j] >= 1, X[i][j] <= 9) for i in range(9) for j in range(9)])
  
9  solver.add([X[i][j] == puzzle[i][j] for i in range(9) for j in range(9) if puzzle[i][j] != 0])
  
10  solver.add([Distinct(X[i]) for i in range(9)])  # Row distinct
11  solver.add([Distinct([X[i][j] for i in range(9)]) for j in range(9)])  # Column distinct
  solver.add([Distinct([X[i + di][j + dj] for di in range(3) for dj in range(3)])
12              for i in range(0, 9, 3) for j in range(0, 9, 3)])  # Subgrid distinct
  
13  if solver.check() == sat:
    model = solver.model()

14    result = [[model.evaluate(X[i][j]).as_long() for j in range(9)] for i in range(9)]

15    return result

  else:
16    return None

if __name__ == "__main__":
  puzzle = [
    [5, 3, 0, 0, 7, 0, 0, 0, 0],
    [6, 0, 0, 1, 9, 5, 0, 0, 0],
    [0, 9, 8, 0, 0, 0, 0, 6, 0],
    [8, 0, 0, 0, 6, 0, 0, 0, 3],
    [4, 0, 0, 8, 0, 3, 0, 0, 1],
    [7, 0, 0, 0, 2, 0, 0, 0, 6],
    [0, 6, 0, 0, 0, 0, 2, 8, 0],
    [0, 0, 0, 4, 1, 9, 0, 0, 5],
    [0, 0, 0, 0, 8, 0, 0, 7, 9]
17  ]

18  solved = solve_sudoku(puzzle)

  if solved:
    for row in solved:
19      print(row)

    # Check if the solution is valid
    if is_valid_sudoku(solved):
20      print("The solution is valid!")

    else:
21      print("The solution is not valid!")

  else:
22    print("No solution found.")

1

Import required components from the Z3 solver library.

2

Check distinct values in row: Ensures each row contains distinct values (1 to 9).

3

Check distinct values in column: Ensures each column contains distinct values (1 to 9).

4

Check 3x3 subgrids: Ensures each 3x3 subgrid contains distinct values.

5

Return True if the solution is valid, otherwise return False.

6

Create a 9 \times 9 matrix of integer variables using Z3’s Int to represent each cell.

7

Initialize the Z3 solver to begin solving the problem.

8

Add constraints to ensure that each cell value is between 1 and 9.

9

Add constraints for the pre-filled cells (the given values from the puzzle) to keep them unchanged.

10

Add row constraints: Each row must contain distinct values.

11

Add column constraints: Each column must contain distinct values.

12

Add subgrid constraints: Each 3x3 subgrid must contain distinct values.

13

Check if the Sudoku is solvable using the Z3 solver.

14

Extract the solution: If a solution is found, extract it from the model.

15

Return the solved puzzle.

16

Return None if no solution is found.

17

Input Sudoku puzzle: A 9 \times 9 grid where 0 represents empty cells.

18

Solve the puzzle: Call the solve_sudoku() function.

19

Print the solved puzzle.

20

Check if the solution is valid using the is_valid_sudoku() function.

21

Print an error message if the solution is not valid.

22

Print “No solution found” if no solution can be found by the solver.

Running the code, Z3 gives us:

5	3	4	6	7	8	9	1	2
6	7	2	1	9	5	3	4	8
1	9	8	3	4	2	5	6	7
8	5	9	7	6	1	4	2	3
4	2	6	8	5	3	7	9	1
7	1	3	9	2	4	8	5	6
9	6	1	5	3	7	2	8	4
2	8	7	4	1	9	6	3	5
3	4	5	2	8	6	1	7	9

Some improvements

Now we’ll modify the code to handle Sudoku grids of different sizes and provide all solutions.

The provided example is a mini Sudoku:

1	0	0	4
0	0	0	0
0	0	0	0
4	0	0	1

And the improved code:

1from z3 import Int, Solver, And, Distinct, Or, sat


# Function to check if a given Sudoku solution is valid
def is_valid_sudoku(solution):
2  n = len(solution)

3  sqrt_n = int(n**0.5)
  
  # Check if each row contains distinct values
  for row in solution:
    if len(set(row)) != n or any(x < 1 or x > n for x in row): 
4      return False
  
  # Check if each column contains distinct values
  for j in range(n):
    col = [solution[i][j] for i in range(n)]  

    if len(set(col)) != n:
5      return False

  # Check if each sqrt_n x sqrt_n subgrid contains distinct values
  for i in range(0, n, sqrt_n):
    for j in range(0, n, sqrt_n):
      subgrid = []  

      for di in range(sqrt_n):
        for dj in range(sqrt_n):
          subgrid.append(solution[i + di][j + dj])

      if len(set(subgrid)) != n:  
6        return False

7  return True

# Function to solve Sudoku puzzles where size is determined from the puzzle
def solve_sudoku(puzzle):
8  n = len(puzzle)
  
9  X = [[Int(f"x_{i}_{j}") for j in range(n)] for i in range(n)]
  
10  solver = Solver()
  
11  solver.add([And(X[i][j] >= 1, X[i][j] <= n) for i in range(n) for j in range(n)])
  
12  solver.add([X[i][j] == puzzle[i][j] for i in range(n) for j in range(n) if puzzle[i][j] != 0])
  
13  solver.add([Distinct(X[i]) for i in range(n)])
  
14  solver.add([Distinct([X[i][j] for i in range(n)]) for j in range(n)])
  
  sqrt_n = int(n**0.5)

  solver.add([Distinct([X[i + di][j + dj] for di in range(sqrt_n) for dj in range(sqrt_n)])
15              for i in range(0, n, sqrt_n) for j in range(0, n, sqrt_n)])
  
16  solutions = []

17  while solver.check() == sat:
    model = solver.model()

18    solution = [[model.evaluate(X[i][j]).as_long() for j in range(n)] for i in range(n)]

19    solutions.append(solution)

20    solver.add(Or([X[i][j] != solution[i][j] for i in range(n) for j in range(n)]))
  
21  return solutions

if __name__ == "__main__":
  puzzle = [
    [1, 0, 0, 4],
    [0, 0, 0, 0],
    [0, 0, 0, 0],
    [4, 0, 0, 1]
22  ]

23  solutions = solve_sudoku(puzzle)

  print(f"Found {len(solutions)} solution(s):")
  for idx, solution in enumerate(solutions):
    print(f"Solution {idx + 1}:")

    for row in solution:
24      print(row)

    print()
    
    if is_valid_sudoku(solution):
25      print("The solution is valid!")

    else:
26      print("The solution is not valid!")

    print()

1

Import required components from the Z3 solver library.

2

Determine the grid size from the solution passed to is_valid_sudoku.

3

Determine subgrid size based on the square root of the grid size (for 4 \times 4, this would be 2x2 subgrids).

4

Check rows: Ensure each row has distinct values between 1 and n.

5

Check columns: Ensure each column has distinct values.

6

Check subgrids: Ensure each subgrid contains distinct values.

7

Return True if all checks pass, meaning the solution is valid.

8

Determine puzzle size from the input list. This makes the function adaptable to any Sudoku size (e.g., 4 \times 4, 9 \times 9).

9

Create integer variables to represent each cell in the Sudoku grid.

10

Initialize the Z3 solver. # <10>

11

Add constraints to ensure each cell’s value is between 1 and n.

12

Add constraints for the pre-filled cells in the puzzle.

13

Ensure distinct values in each row.

14

Ensure distinct values in each column.

15

Ensure distinct values in each subgrid.

16

Initialize list to store all solutions.

17

Check if the puzzle is solvable using Z3’s sat check.

18

Extract the solution from the model if it’s solvable.

19

Store each solution in the solutions list.

20

Add constraint to ensure the solver does not return the same solution again.

21

Return all found solutions.

22

Define a 4 \times 4 Sudoku puzzle. Empty cells are represented by 0.

23

Solve the puzzle and automatically determine the size.

24

Print each solution.

25

Check if the solution is valid using the is_valid_sudoku() function.

26

Print validation result for each solution.

The output has two solutions:

Solution 1

1	3	2	4
2	4	1	3
3	1	4	2
4	2	3	1

and

Solution 2

1	2	3	4
3	4	1	2
2	1	4	3
4	3	2	1

Have fun extending code to KenKen o Kakuro puzzles, or others you like! Enjoy!

References

Papers

Leonardo Moura and Nikolaj Bjørner. 2009. Satisfiability Modulo Theories: An Appetizer. Formal Methods: Foundations and Applications: 12th Brazilian Symposium on Formal Methods, SBMF 2009 Gramado, Brazil, August 19-21, 2009 Revised Selected Papers. Springer-Verlag, Berlin, Heidelberg, 23–36. DOI

Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C. (2004). DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds) Computer Aided Verification. CAV 2004. Lecture Notes in Computer Science, vol 3114. Springer, Berlin, Heidelberg. DOI

Barrett, C., Sebastiani, R., Seshia, S. A., & Tinelli, C. (2009). Satisfiability modulo theories. In Handbook of Satisfiability (1 ed., pp. 825-885). (Frontiers in Artificial Intelligence and Applications; Vol. 185, No. 1). IOS Press. DOI

Books

Yurichev, D. (2024). SAT/SMT by example. Self-published. Online.

If you’re curious about SAT (Boolean Satisfiability) and SMT (Satisfiability Modulo Theories) solvers but don’t want to wade through dense theory, SAT/SMT by Example by Dennis Yurichev is a great pick. This book is all about showing you how to use these solvers in real-world scenarios, with loads of practical examples and hands-on exercises. It’s basically the “learn by doing” approach, which is perfect if you want to see how these tools can solve actual problems without getting lost in too much math.
One of the best things about this book is how approachable it is. Yurichev explains things in a straightforward way, making it easy for beginners to pick up on the basics. You’ll get examples that walk you through how to use solvers like Z3, a popular SMT solver, and you’ll find the code snippets helpful if you’re the type who likes to tinker. That said, the book doesn’t shy away from diving deeper. If you already have some experience or are looking to understand more complex topics like symbolic execution or program verification, you’ll find plenty here to chew on. The chapters build on each other nicely, so you won’t feel like you’re being thrown into the deep end without a float.
This isn’t a book that’s going to overwhelm you with theoretical details. Instead, it’s packed with practical examples—actual problems and code solutions that show how SAT and SMT solvers are used in real applications. One big plus: the book is free! Yurichev made it available online for anyone to download. This makes it super accessible, whether you’re a student, researcher, or hobbyist. It’s great to have a resource like this that doesn’t put a paywall between you and learning, and the fact that it’s frequently updated makes it even better.
While the book covers a lot, it’s pretty focused on Z3, so if you’re looking to learn about other solvers, you might need to supplement with other materials. Also, while it’s beginner-friendly, if you’re totally new to programming or logic, some parts might take a couple of reads to really sink in. But Yurichev’s writing style is clear enough that you’ll probably catch on without too much struggle.

Kroening, D., & Strichman, O. (2016). Decision procedures: An algorithmic point of view (Texts in Theoretical Computer Science. An EATCS Series). Springer-Verlag Berlin Heidelberg. DOI

Tutorials

Bjørner, N., de Moura, L., Nachmanson, L., & Wintersteiger, C.. Programming Z3. Microsoft Research. Online.

This tutorial provides a programmer’s introduction to the Satisfiability Modulo Theories Solver Z3. It describes how to use Z3 through scripts, provided in the Python scripting language, and it describes several of the algorithms underlying the decision procedures within Z3. It aims to broadly cover almost all available features of Z3 and the essence of the underlying algorithms.

Z3 Guide.

Online tutorial of Z3 from Microsoft.

Standards

SMT-LIB.

SMT-LIB is a standard format and set of benchmarks used for specifying and solving problems in the context of SMT. The purpose of SMT-LIB is to: 1. Standardize the Language: It provides a uniform language for writing problems and formulas to ensure that different SMT solvers can understand the same input format. This allows solvers to be compared and used interchangeably on the same problem sets.
2. Encourage Solver Development: By offering a large set of standardized benchmarks, SMT-LIB promotes the development of more efficient SMT solvers, as developers can use these benchmarks to test and improve their tools.
3. Promote Research and Collaboration: Researchers can use SMT-LIB as a shared resource for testing new theories, algorithms, and solvers. It facilitates collaboration by offering a common platform for problem instances, making it easier to compare results.
4. Provide Tool Support: SMT-LIB includes support for specifying problems, as well as querying and interacting with SMT solvers, helping in automation and making solvers more accessible in various fields, including verification, artificial intelligence, and formal methods.
SMT-LIB is widely used in applications such as software and hardware verification, automated reasoning, formal methods, and program analysis.

Code

Z3.

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

cvc5.

cvc5 is an efficient open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the satisfiability (or, dually, the validity) of first-order formulas with respect to (combinations of) a variety of useful background theories. It further provides a Syntax-Guided Synthesis (SyGuS) engine to synthesize functions with respect to background theories and their combinations.