This semester, in our **Combinatorial Decision Making and Optimization** course, we were lucky enough to be able to face another interesting challenge: the optimization of the placement of circuits on a chip.

This problem is strictly tied with the technological progress we’ve witnessed in the last decade: research made it possible to reduce the transistors’ size, but the placement of the actual circuits remains a non-trivial challenge.

Basically, what we wanted to achieve was finding a programmatic way of placing circuits in the least amount of space:

Our tool belt featured 3 different techniques:

**Constraint Programming****SAT solving****SMT solving**

Even though these tools can solve the same tasks, they are inherently different and deserve way more explanations than the ones I’ll provide here.

## How we decomposed the problem

Many different solutions are findable for this task. Starting from the fact that global constraints are usually well implemented and will often perform better than custom-tailored solutions, we explored those available in MiniZinc, an open-source Constraint Modeling language.

Even though there exists a global constraint which encodes this exact problem, *diffn, *we found a different approach to be more performing: approaching the problem in one dimension first, then the other.

This is done through the *cumulative *constraint, a constraint that is used for **task scheduling**: the computer has tasks to execute, each having an execution time and a resource consumption . The computer obviously has a *resource constraint *which can’t be exceeded.

This partial solution allows us to break lots of symmetries: many solutions share the same Y coordinates, meaning that their objective function’s value (in this case, the height of the chip) is the same.

Moreover, solving the Y coordinates first, we get the minimum height possible: we then just have to **satisfy **the X constraints and not **optimize**. This makes the second constraint solution really easy to get.

### Variables’ ranges

We are still missing a pretty important part of our problem definition: the variables’ ranges. Having a well-made range for the variables we’re searching allows us to stop the search as soon as we find an optimal solution, reducing the size of the search tree.

First of all, the *task start times *can span from to , with this last value being equal to .

Intuitively, we know that in the worst case, we’ll execute the tasks one at a time: the maximum start can therefore be the last start of the worst case.

For the same reason, the objective function (the height of the chip) has an upper limit of .

The lower bounds are much more important tough. When circuits can be arranged without empty space, we have found the optimal solution. To know the height of this optimal solution, we can just divide the area of the circuits by the width, keeping in mind that if it is not perfectly divisible, we’ll have to add 1.

## Encoding the different models

### MiniZinc

**MiniZinc makes it really easy to encode a model. **Once we have preprocessed the input file using a little Python script, we can directly use the model with *MiniZincPy. *What is really interesting is that the MiniZinc implementation of *cumulative *uses **Lazy Clause Generation, **which speeds it up a lot. This technique is basically a mix of Finite Domain propagation and SAT theory. You can read more about it in this really interesting paper by Schutt et al.

MiniZinc even offers the possibility of choosing among different solvers. To exploit LCG, we use **Chuffed**, a solver which was created exactly for this.

### SAT solving

While **Constraint Programming provided really good results** in the test runs, another possibility is definitely interesting to explore: **SAT solving**. **SAT** stands for **Satisfiability in Boolean Satisfiability,** namely one of the most discussed logic and computer science problems ever. With satisfiability, we’re asking whether **a valid interpretation can be found** for a given **Conjunctive Normal Form boolean formula**. This was the first problem to ever be proved NP-complete. Since, as already mentioned, **no polynomial-time solution has been found** yet (and might never be), heuristics algorithms have been proposed, being able to solve several-thousand variables problems in acceptable times. As by definition, **any NP-complete problem can be reduced to SAT**, these heuristic algorithms provide an exceptional tool for the solution of complex problems in computer science. *Very Large Scale Integration* is among these.

As SAT solvers were **not born to actually optimize problems** but just to satisfy them, we’re going to need a *branch and bound *approach: when we find a solution, we add a constraint imposing that the next one has to be better.

The *cumulative *encoding in SAT is the following: we introduce Boolean variables that tell whether a task is active at time . Then, we can first impose the resource constraint: the sum of the active tasks’ requirements cannot be higher than the resource maximum.

The next step is imposing that durations are taken into account: if a task starts being active at time , it has to be active until .

Having found the Y coordinates, we can find the X coordinates by satisfying a model which introduces the second coordinate: we now have Boolean variables stating that task is the one found at . Obviously, no other task can be.

### SMT solving

As it is pretty clear by now, **SAT solvers are great tools** in terms of performances, explainability and availability on the market. The great successes that have been reached thanks to SAT solvers are **motivation for its frequent use** in diverse domains, but still, as mentioned before, the** encoding remains the most time-consuming and complex** part. It would therefore be nice to be able to **express problems with a richer language**: **logics** rather than *propositional logic*. Obviously, this takes into account some **loss of efficiency**, but the expressivity of the model encoding might actually make it easier to improve solutions, and consequently, outperforming SAT. **Satisfiability Modulo Theories** solvers are the answer we are looking for: they allow the programmer to **define a problem in what is, roughly, first order logic**, then autonomously solve the instance. The eager approaches consisted in a translation to an equivalent SAT instance, while nowadays SMT solvers are much more complex tools that tightly integrate DPLL-style boolean reasoning with theory-specific solvers. SMT solvers allow us to define models that are similar to the ones seen in Lazy Clause Generation solving: in SMT, we can mix boolean variables and finite domain constraints as it’s done in LCG. As done before, we’ll encode the cumulative constraint, then simply satisfy the model to find the missing coordinate.

The literature for cumulative is way more dense than the one someone can find for VLSI. A breakthrough paper in the topic is *Why cumulative decomposition is not as bad as it sounds*, which explained how **Lazy Clause Generation** can be a great solution for this task. Even though we would need a Lazy Clause Generation solver like Chuffed to really enjoy the performance increase in these models, we **still can implement them in an SMT instance** obtaining good results. The paper proposes two different encodings, differing in the number of Boolean variables and constraints: **Time-RD, **which for every time t constrains the sum of all resource requirements to be less or equal to the resource capacity, and **Task-RD, **a relaxation of the first model only ensuring a non-overload of resources at the start times.

We chose to implement the second one, using **Z3**, an SMT solver by Microsoft. More specifically, we used the Python wrapper Z3Py, which made everything easy and straightforward.

## Code and report

All the code is, as always, open-source, and can be found here. The PDF report for the project, containing further explanations to the concepts presented in this article, can be found here.

**Thanks for reading!**