Examples

Problem Modelling

Graph Coloring

For a first modelling example we will take a look at some graph coloring in a simple setup with 5 nodes.

To represent this graph in SATish we write an array declaration foolowed by its structure initialization.

# Number of verties in the graph.
n = 5;

# Graph representation
neigh[n][n] = {
   (1,1) : 0,
   (1,2) : 0,
   (1,3) : 1,
   (1,4) : 1,
   (1,5) : 1,

   (2,3) : 1,
   (2,4) : 1,
   (2,5) : 1,

   (3,4) : 1,
   (3,5) : 1,

   (4,5) : 0
};

In this case, all array entries are constants. Next, we declare our problem unknowns, the color assignment for each vertex and also the list of used colors.

# Correspondence between each vertex and its color
vc[n][n];

# Used colors, a quantity we wish to minimize.
c[n];

Now, we state the constraints that well define the graph coloring problem. First of all, it is fundamental that neighbours \(i\) and \(j\) do not share a same color \(k\).

(int) neighbour_coloring[2]:
    forall{i = [1:n]}
    forall{j = [1:n], j > i}
    forall{k = [1:n]}
    neigh[i][j] -> ~(vc[i][k] & vc[j][k]);

It is also important to keep track of the colors being used, that is, for each vertex \(i\) dyed with a color \(k\) we say that \(k\) is used.

That yields the logical expression \(\forall i \,\, \forall k \,\, vc_{i, k} \implies c_{k}\).

(int) use_color[1]:
    forall{i = [1:n]}
    forall{k = [1:n]}
    vc[i][k] -> c[k];

Following, we say that to every vertex must be assigned a unique color, where we may use the wta quantifier keyword i.e. there exists exactly one color \(k\) related to vertex \(i\).

(int) color_all[1]:
    forall{i = [1:n]}
    wta{k = [1:n]}
    vc[i][k];

Last but not least, we define our optimality constraint, where we state that every color used increases the overall cost.

(opt) cost: sum{k = [1:n]} c[k];

Note: The whole graph_color.sat file is available for downaload here.

Travelling Salesman Problem

One more graph-oriented example will be a Travelling Salesman Problem (TSP) instance with 4 cities.

We start by representing our graph structure. As the starting position doesn’t matter f or the problem formulation, we duplicate the first town, thus creating a ghost town, intended to be the last on the tour. The ghost town has the same connections as its twin and the distance between this two is zero, as is the distance between any node to itself.

n=5;

dist[n][n] = {
   (1,1): 0,
   (1,2): 4,
   (1,3): 4,
   (1,4): 9,
   (1,5): 0,

   (2,1): 4,
   (2,2): 0,
   (2,3): 9,
   (2,4): 4,
   (2,5): 4,

   (3,1): 4,
   (3,2): 9,
   (3,3): 0,
   (3,4): 4,
   (3,5): 4,

   (4,1): 9,
   (4,2): 4,
   (4,3): 4,
   (4,4): 0,
   (4,5): 9,

   (5,1): 0,
   (5,2): 4,
   (5,3): 4,
   (5,4): 9,
   (5,5): 0
};

tour[n][n]; # (town, tour position) pairs

We defined also a tour structure, which assigns every town a position on the tour. Also, it is important to clamp the mirrored towns to the tour’s endpoints.

# Low Penalty Level
LOW = 1;

# Fix both endpoints (the first town and its ghost town)
(int) mirror_town[LOW]: tour[1][1] and tour[n][n];

Another option would be to define these boudaries directyle into the tour declaration.

tour[n][n] = {
    (1, 1): 1,
    (n, n): 1
};

All other entries are left as variables.

The sole integrity constraint to be guaranteed is that every town occupies a single position on the tour. Conversely, every turn must be assigned to a single town.

(int) visit_all_once[LOW]:
   # Every city 'i' appears uniquely across the tour.
   forall{i = [1:n]}
   wta{j = [1:n]}
   tour[i][j];

(int) fill_all_once[LOW]:
   # Every tour position 'i' has exactly one city 'j' associated to it.
   wta{i = [1:n]}
   forall{j = [1:n]}
   tour[i][j];

The optimality constraints are built upon accounting for the costs that lie between nodes who are neighbours on the tour. This must be done twice in order to handle assymetrical setups.

(opt) backwards_cost:
    sum{i = [1:n]} # for each city 'i'
    sum{j = [1:n], i != j} # for each other city 'j'
    sum{k = [2:n]} # for each position
    (tour[i][k] and tour[j][k-1]) * dist[i][j];

(opt) forwards_cost:
    sum{i = [1:n]} # for each city 'i'
    sum{j = [1:n], i != j} # for each other city 'j'
    sum{k = [1:n-1]} # for each position
    (tour[i][k] and tour[j][k+1]) * dist[i][j];

Note: The whole tsp.sat file is available for downaload here.

Knapsack

The Knapsack Problem involves some extra tricks when written in SATish. Its usual formulation is indeed very straightforward and is usually referred to as one of the first steps in the combinatorial optimization kindergarten.

Take \(n\) items, where each one has an associated weight \(w_{i}\) and value \(v_{i}\). One wants to maximize the total carried value without surpassing the knapsack’s capacity \(M\).

\begin{array}{c c} ~ & \displaystyle \max \sum_{i = 1}^{n} x_{i}\, v_{i}\\ \text{s.t.} & \displaystyle \sum_{i = 1}^{n} x_{i}\, w_{i} \le M \end{array}

Let’s suppose we have three items with the following weights and values to fit in a knapsack with size \(M = 4\).

\(w_{i}\)	\(v_{i}\)
\(1\)	\(4\)
\(4\)	\(6\)
\(3\)	\(3\)

n = 3;

x[n];
w[n] = {(1) : 1, (2) : 4, (3) : 3};
v[n] = {(1) : 4, (2) : 6, (3) : 3};

M = 4;

To achieve the declaration of the viability constraint in our framework it is necessary to transform inequalities into equality relations. We can do that by introducing a few auxiliary variables. We write

\begin{align*} \sum_{i = 1}^{n} x_{i}\,w_{i} + s = M \end{align*}

where \(0 \lt s \le M\) is represented through its binary expansion

\begin{align*} s = \sum_{j = 1}^{m} 2^{j-1}\, s_{j} \end{align*}

that is, \(m = \log_{2} M\) and \(s_{j} \in \mathbb{B}^{m}\).

That said, the problem can be stated as

\begin{align*} \min -\sum_{i=1}^{n} x_{i}\, v_{i} + \lambda \left({ \sum_{i=1}^{n} x_{i}\, w_{i} + \sum_{j=1}^{m} 2^{j-1}\, s_{j} - M }\right)^{2} \end{align*}

for some penalty \(\lambda\) which might be left for Satyrus to compute.

n = 3;

x[n];

w[n] = {
    (1) : 1,
    (2) : 4,
    (3) : 3
};

v[n] = {
    (1) : 4,
    (2) : 6,
    (3) : 3
};

s[2];

# Capacity
M = 4;

# Penalty Levels
LOW = 1;

(opt) eita[LOW]: (x[1] * w[1] + x[2] * w[2] + x[3] * w[3] + (s[1] + 2 * s[2]) - M) ** 2.0;

(opt) cost: sum{i = [1:n]} -v[i] * x[i];

Note: As of version 3.0.7, there is no available syntax for writing the general form of this problem as is in SATish, due to the lack of inner loops. This feature is scheduled to be present on the first release of the 3.1.x series. A future version will allow one to write the constraints from the code above as

# Capacity
M = 4;

# Log_2 M
m = 2;

s[m];

# Penalty Levels
LOW = 1;

(opt) eita[LOW]: ((sum{i=[1:n} x[i] * w[i]) + (sum{j=[1:m]} 2**(j-1) * s[j]) - M) ** 2.0;

(opt) cost: sum{i = [1:n]} -v[i] * x[i];

Compilation

As the source file is complete, one could simply run

$ satyrus graph_color.sat

This will output the graph_color.json file, with an array object containing in each entry a “term” array of unknowns and its respective multiplicative constant “cons”. If there is any constant term, its value for the “term” key will be null.

This is intended to represent the problem’s energy equation.

Note: It is possible to set the output destination using the -o, --ouput option, followed by the desired target.

Solver Interfaces

Solver interfaces, available via the Satyrus Python API allow the user to interact with the compilation output in many different ways, from straightforward passing it into solver machinery to conversion between output types. In order to pass the generated energy equation to a solver, it is enough to use the -s, --solver option.

$ satyrus source.sat -s solver

The expected behaviour is to store the solution in the source.out.json file, under keys “solution” and “energy”, where the first is a mapping between variables and its values and the latter is the total energy for the given setup.

Note: Run sat-api for a list of the available solvers in your installation.

Parameters may be passed to the solver using a separate JSON file containing the corresponding mapping. The destination for feeding the parameters file must be provided using the -p, --params command-line option.

When running the dwave solver, it is possible to specify both num_reads and num_sweeps by providing the dwave.json file as follows:

{
   "num_reads": 1000,
   "num_sweeps": 10000
}

and then, by typing the right command and hitting enter.

$ satyrus graph_color.sat -s dwave -p dwave.json

Custom API Setup

Defining custom solver interfaces is pretty straightforward. In a separate Python file, import the SatAPI type from the satyrus package and subclass it as shown below:

from satyrus import SatAPI, Posiform
import random

class bogo(SatAPI):

    def solve(self, energy: Posiform, **params: dict) -> tuple[dict, float]:
        X = energy.variables
        s = {x: random.randint(0, 1) for x in X}
        e = float(energy(s))
        return (s, e)

Your new class must implement the solve method, which must have one of the two signatures presented above. It receives a Posiform object and some eventual parameters as keyword arguments. If the return type is a tuple containing a solution mapping and its respective energy, the solution is considered to be complete, receiving special formatting when delivered to the output file. Otherwise, a string representation of the output object is dumped to the target destination as-is.

After writing the contents above to the bogoapi.py file, it becomes possible to include the custom interface by typing

$ sat-api add bogoapi.py
$ satyrus graph_color.sat -s bogo

Note: As you might be thinking, it is important to chose the class name wisely!

More in-depth explanation about the Python API is found on this page.