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 n tasks to execute, each having an execution time t and a resource consumption r. 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 0 to s_{max}, with this last value being equal to \sum_{i=1}^{n} d_{i}-\min _{i=1 \ldots n} d_{i}.

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 h (the height of the chip) has an upper limit of \sum_{i=1}^{n} d_{i}.

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.

h_{\min }=\left\{\begin{array}{ll}\sum_{i=1}^{n} x_{i} y_{i} \div w & \text { if } \sum_{i=1}^{n} x_{i} y_{i} \quad \bmod w=0 \\ \left(\sum_{i=1}^{n} x_{i} y_{i} \div w\right)+1 & \text { otherwise }\end{array}\right.

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 nt_{max} Boolean variables B_t^i that tell whether a task i is active at time t. Then, we can first impose the resource constraint: the sum of the active tasks’ requirements cannot be higher than the resource maximum.

\bigwedge_{i=0}^{i \leq t_{\max }}\left(\sum_{t=0}^{t \leq n} r_{t} \leq r e s_{\max }\right)

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

Having found the Y coordinates, we can find the X coordinates by satisfying a model which introduces the second coordinate: we now have w \cdot h \cdot c Boolean variables B_{x,y}^i stating that task i is the one found at x,y. 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!