- English only

# Lab for Automated Reasoning and Analysis LARA

### Handout

Download the constraints.zip handout archive file and extract it somewhere on your machine. Then, follow the instructions on how to setup up the git repository for this project.

### Constraints

In this assignment, you will implement a basic constraint generator for a classic scheduling problem.

As in the previous assignments, you are encouraged to look at the Scala API documentation while solving this exercise, which can be found here:

### Scheduling Balélec

The last standing green space at EPFL, the Esplanade, has been converted into a construction site for fancy buildings for non-engineers. As a result, the Balélec committee is rushing to find a new spot for this year's festival, and needs your help for taking care of the logistics. You are in charge of assigning stages to the artists (bands) and tasks to volunteers.

In this assignment, you will get to encode this instance of a scheduling problem as a propositional constraint solving problem, which you will then ship to CafeSat, a SAT solver written in Scala.

SAT is one of the most famous problem in computer science. The problem is to find a satisfiable assignment to a boolean circuit. That is, assigning each boolean variable to true or false such that the whole circuit final value is true. In this homework, we will explore some applications of SAT to more concrete computing problems.

### Warmup : Sat Solving with CafeSat

A SAT solver is a tool designed to solve the SAT problem. It takes as input a propositional formula with variables, and its output is either an assignement to the variables that makes the whole formula true, or a proof that no such assignment exists. We will use CafeSat, a small SAT solver written in Scala which has the advantage of being easy to use from a Scala program. You should not spend too much time trying to understand how a SAT solver works, this would deserve a whole course in itself, but simply focus on how you can create formulas and ask the solver to find a satisfying assignment.

#### CafeSat Tutorial

Before delving into the API of CafeSat, let's look at a very simple example. Consider the following program:

import cafesat.api._ import FormulaBuilder._ import Formulas._

val a: PropVar = propVar() val b: PropVar = propVar() val f: Formula = a && (!a || b) Solver.solveForSatisfiability(f) match { case None => { println("There is no solution") } case Some(model) => { println("a is: " + model(a)) println("b is: " + model(b)) } }

First we introduce two propositional variables `a`

and `b`

, using the generator
function `propVar`

. `propVar`

always generates a new fresh variable. Then we
build a formula by combining those variables with boolean operators `&&`

, `||`

and `!`

. The formula we are creating is very simple and is the conjunction of
two terms: the first one states that `a`

must be true and the second one states
that either `a`

must be false or `b`

must be true. Such a formula is true when
`a`

and `b`

are both true.

We then invoke `Solver.solveForSatisfiability`

on that formula. `solveForSatisfiability`

returns an `Option[Model]`

, which is `Some(model)`

if the formula can be satisfied,
and `None`

if it unsatisfiable. In the above example, `solveForSatisfiability`

returns
a `Model`

that maps both `a`

and `b`

to `true`

.

#### The CafeSat API

Scaladoc for CafeSat is available here.

The CafeSat API is straightforward. It provides helper operators to build a formula
tree, and then expose a `solveForSatisfiability`

function to resolve it.
You introduce fresh propositional variables by calling
`propVar()`

, typically you can assign them to a Scala value:

val p: PropVar = propVar()

If you call the `propVar`

function with a string parameter, a propositional variable with the string
as a prefix will be created.

You can also create the trivial formulas `true`

and `false`

. Writing the following:

val f: Formula = false

will trigger an implicit conversion from the values of type `Boolean`

to a
`Formula`

. (If you are interested in how implicit conversions, also known as
the Pimp My Library pattern, work, take a look at this
documentation).
Usually, you should only need a literal `true`

/`false`

when you are building formulas
from a Scala data structure like a `List`

, for example as a starting value of a `foldLeft`

:

val fs: List[Formula] = ??? val disj: Formula = fs.foldLeft[Formula](false)((acc, el) => acc || el)

You can build arbitrary propositional `Formula`

-s by using operators on
`Formula`

s: `&&`

(AND), `||`

(OR), `!`

(NOT), and `iff`

. You can also use the
functions `and`

and `or`

(defined in `FormulaBuilder`

) which take a variable
number of formulas:

val f: Formula = and(p, q, r)

This formula is equivalent to

val f = p && q && r

Finally, calling `solveForSatisfiability(f)`

will invoke the SAT solver on the
formula `f`

. The return type is an `Option[Map[PropVar, Boolean]]`

: `None`

if
the formula cannot be satisfied, and `Some(model)`

with `model`

providing a
mapping of propositional variables to `true`

/`false`

, such that the formula `f`

is true. You can only query the model for propositional variables introduced by
`propVar()`

. Note that the model will only provide a mapping for variables
present in the formula `f`

. It is possible that the returned value by
`solveForSatisfiability`

is `Some(Map())`

, which literraly means that the
formula is satisfiable with an empty model. This can happen if you send a
formula without any variable to the solver, such as the literal `true`

, or some
combination of it such as `true || false`

.

#### Building Circuits

Let's look at a bigger program that is using CafeSat. Consider the following circuit:

Take a look at the `Circuits.scala`

in your project. The `solveExample`

function defines and solves the above circuit.

We first introduce propositional (boolean) variables using the
`cafesat.api.FormulaBuilder.propVar()`

function for every wire. The value
`circuit`

constructs a propositional formula from these variables. This formula
is a large conjunction with one conjunct for each of the gates. The overloaded
operators `&&`

, `||`

and `!`

create formulas for conjuntion, disjunction and
negation, respectively. Note also the `iff`

operator for introducing an
if-and-only-if constraint.

Be careful not to confuse the Scala value introduced with `val p = …`

and the
*propositional variables*, which are the building blocks for formulas and are introduced by `propVar(“p”)`

.
Each call to `propVar`

introduces
a fresh propositional variable that you can use to build formulas. Usually you also need to keep
a reference (often, as a Scala `val`

) to refer to formula variables. Note that

val x: PropVar = propVar("p") val y: PropVar = propVar("p")

will result in `x`

and `y`

referring to two distinct fresh variables.

As a first exercise, run the `constraints.Circuits`

file, and inspect the
output. You can play around with the list of constraints (the `circuit`

value). What happens if you force `p`

to be `true`

, by adding `p`

as an
additional constraint? What if `q`

is forced to be `true`

?

For a more advanced example, there is a Sudoku solver implemented with CafeSat. You can take a look at the sudoku solving code.

Now you are ready to start helping the Balélec committee!

#### Part 1: Bands and Stages

Let us first look at scheduling concerts. We have a number of bands, time
periods, and stages. We need to fit all the bands over the evening. We call a
pair of a time period and a stage a **slot**.

For each band, there is a set of slots in which they can play. For example, some bands need a large stage, or only wake up at 10pm.

You will be required to implement a function `plan`

which takes as input the
`preferences`

map, associating a `List`

of possible slots for each band. Your
task is to complete the implementation of this function such that it returns a
complete mapping of bands to slots, if such an assignment is possible, or
`None`

if impossible. The mapping should assign a unique and different slot to
each band, and that slot has to be present in the `preferences`

of the band. In
general, there could be more than one solution; in that case, any valid
assignment can be returned. The function should not return partial solution,
if this is impossible to find a complete valid assignment for a given
`preferences`

, then the function should return `None`

.

This problem could be solved by a tailor-made algorithm, such as a naive brute-force search. However the goal of this homework is to introduce you to declarative programming, in which you state the problem as a set of constraints, and rely on an external engine to solve them and derive a solution from it. As this is a rather new concept to most of you, we have decomposed the problem into very precise steps to help you. But it is still good to keep the big picture in mind.

##### Strategy for encoding the problem

We introduce a propositional variable x(i, j) for each band i and slot j. The propositional variable x(i, j) states that band i plays in slot j. Now we can build a SAT problem involving these variables, and a solution to it can be mapped back to an assignment of bands to slots.

In a valid assignment, each band gets a different slot, so the goal of the constraints sent to the SAT solver is to ensure that exactly one variable per band is assigned to true, and at most one variable per slot is assigned to true. Additional constraints are needed to ensure that the band is playing in one of its desired slots.

We provided the basic structure of the function, We store the propositional variables in a mapping from the pairs of band-slot, for easy access while building the constraints.

We also provided the code for mapping back a satisfying assignment from the solver into an assignment of bands to slots. You should make sure you understand how this structure works, before implementing the generation of constraints.

Before proceeding to the actual encoding of the problem, we need to create the
mapping from the pairs of band-slot to propositional variables. In order to do
so, we need the list of all the bands and all the slots. We can extract those
from the `preferences`

parameter. As an easy warm-up, we ask you to implement
a small utility function that extracts all the different slots from the
`preferences`

map.

def getAllSlots(preferences: Map[Band, List[Slot]]): Set[Slot] = ???

This function should take the `preferences`

as a parameter, and return a
`Set[Slot]`

containing all the different slots available. Keep in mind that
each band might be assigned to a different list of slots, with some of the
slots shared by several bands.

##### Constraints ensuring each band gets a desired slot

We need to ensure that each band can be assigned only to slots that are
desirable for them. Define the `desirableSlots`

value. For each band that is
part of the `propVariables`

, it will yield a constraint such that the band in
question can only be assigned to a slot which is part of its preference list.
The `desirableSlots`

value is a sequence of formulas, one formula per band.

val desirableSlots: Seq[Formula] = ???

**Note**: there are many possible ways of implementing `desirableSlots`

. You
can either ensure that a band gets one of its desired slots, or gets none of
the undesirable slots. Either way, you will have to ensure that each band gets
**at least one** slot.

##### Constraints ensuring each band plays at most once

We next need to ensure that a band cannot play twice. Define the `eachBandPlaysOnce`

value for this. Once again, its type is `Seq[Formula]`

.

val eachBandPlaysOnce: Seq[Formula] = ???

Hint: Given a list of formulas f1, f2, …, fn, an equivalent way to state that at most one is true is to say that there is no pair of formulas such that both are true:

(!f1 || !f2) && (!f1 || !f3) && (!f2 || !f3) && ???

##### Constraints ensuring each slot is used at most once

Finally, we need to ensure that a slot cannot be occupied by more than one
band. Define the `eachSlotUsedOnce`

value which describes this as a sequence of
formulas:

val eachSlotUsedOnce: Seq[Formula] = ???

With this, you should be able to run some tests in the `ConcertsPlannerSuite.scala`

file.

#### Part 2: Arithmetic with SAT

Congratulations! Each band has been assigned to a slot. The Balélec committee is impressed, and wants you to assign volunteers to different tasks now. Every task needs a certain number of volunteers (can be more than one), and every volunteer can do a certain amount of tasks (can be more than one).

You may have noticed that arithmetic operations are not supported in propositional logic directly: the SAT solver works only with boolean variables. Despite its apparent simplicity however, SAT is extremely general, and many problems can be reduced to it.

While we could use a more general solver (for example, an SMT solver that can be accessed through scala-smtlib library) for encoding numerical constraints, here we will see how to encode them using propositional logic. Essentially, we will be generating boolean circuits for addition and comparison. By solving this problem, you will also get an idea how one can automatically generate hardware circuit descriptions using Scala (an idea pushed much further in the Chisel domain-specific language).

##### Warmup bis: integer to binary conversion, and vice-versa

In `Arithmetic.scala`

, implement the `int2binary`

and `binary2int`

functions.
As their names suggest, they convert a positive integer to its binary representation,
and vice versa, respectively.

def binary2int(n: List[Boolean]): Int = ??? def int2binary(n: Int): List[Boolean] = ???

Make sure that your `int2binary`

function does not return any unnecessary
leading `false`

elements in the list. You must encode `1`

to `List(true)`

and
not to `List(false, true)`

which would be a valid encoding of `1`

but with a
redundant leading `false`

. However, `0`

is encoded as `List(false)`

so the
result could start with a `false`

. On the other hand, your implementation of
`binary2int`

should be flexible enough to support inputs with unnecessary
leading zeros. It means that `binary2int(List(false, true))`

should return
the same thing as `binary2int(List(true))`

, which should return `1`

.

##### The ''lessEquals'' circuit

Now we will start to use `List[Formula]`

as a way to represent a symbolic
number. Essentially, a variable could be represented in its binary
representation with n propositional variables representing whether each
bit is 1 (`true`

) or 0 (`false`

). Our goal is then to implement a few basic
arithmetic operations working with that representation.

We will start with the less than or equals circuit. Given two numbers
represented as lists of formulas, implement the `lessEquals`

function that
creates a formula that is true if and only if the first parameter is less than
or equal to the second parameter:

def lessEquals(n1: List[Formula], n2: List[Formula]): Formula

Here the list of `Formula`

represents the bits of the numbers. However, they
are symbolic: notice how the result is a `Formula`

as well, it is not a
`Boolean`

. Whether the result is `true`

or `false`

will depend on the exact
assignment of the variables. It may help you to think of how you would draw an
electronics circuit for this function before you get started with the
implementation.

Let's look at an example to make things clearer. Think of one-bit numbers, you
would get as input two numbers represented respectively by `List(a1)`

and
`List(a2)`

, with `a1`

and `a2`

propositional variables. When is `List(a1)`

smaller or equals to `List(a2)`

? Certainly it is if `a1`

is `false`

, as `n1`

is then `0`

. It could also happen if `a1`

is true and `a2`

is true. The actual
formula that define this relation is then: `!a1 || (a1 && a2)`

, which is the
`Formula`

that `lessEquals`

should return in that case.

Notice how we assume that the bits `a1`

and `a2`

were propositonal variables.
The truth is that they are defined as `Formula`

, so they do not have to be
propositional variables. They could be boolean combination of variables, such
as `a1 || a2`

. Or they could actually be concrete values, `true`

or `false`

.
However you cannot assume anything on them and should generate the most general
`Formula`

. Look at what happens in the above example if we were to replace `a1`

by the value `false`

. In that case, `lessEquals`

would receive `List(false)`

and `List(a2)`

as arguments, and using the derived formula above, it would
return `!false || (false && a2)`

. Notice that this is a perfectly fine answer,
because it actually simplifies to `true`

, which is indeed to be expected when
`n1`

is `List(false)`

, the encoding of `0`

.

Finally, be careful that `n1`

and `n2`

do not have to be of the same length.
For example, `n1`

could be `List(a1, a2)`

and `n2`

could be `List(b2)`

. Does it
mean that `n1`

is necessarly bigger than `n2`

? No, you cannot assume so. If
`a1`

happens to be `false`

, then we must compare `a2`

and `b2`

. However, if
`a1`

is true, then it is always the case that `n1`

is bigger than `n2`

. The
result should then be `!a1 && (!a2 || (a2 && b2))`

.

##### The adder circuit

Start with implementing the `fullAdder`

circuit:

def fullAdder(a: Formula, b: Formula, cIn: Formula): (Formula, Formula) = ???

Which essentially computes the sum of three 1-digit numbers. You may find the
following Wikipedia page about the adder
useful when implementing this function. The role of the `fullAdder`

is to provide
one step of the addition, where the first element of the pair that you return is
used as the carry for the next step.

Now we should be able to implement the `adder`

circuit. First, let's look at a naive
implementation:

def naiveAdder(n1: List[Formula], n2: List[Formula]): List[Formula] = { require(n1.size == n2.size) (n1, n2) match { case (x::Nil, y::Nil) => { val (head, last) = fullAdder(x, y, false) head :: last :: Nil } case (x::xs, y::ys) => { val z::zs = naiveAdder(xs, ys) val (head, second) = fullAdder(x, y, z) head :: second :: zs } case _ => sys.error("Unexpected case") } }

This implementation seems straightforward and you can use it as an inspiration for your solution. However it suffers from one major issue that we will explain below. Keep also in mind that your implementation needs to handle addition of two numbers that may have a different number of digits.

The main issue with the above implementation is that the inductive case return
complex subformulas as part of the result number. As you can see, the `head`

and
`second`

expression are used as the elements of the result. However, `head`

and
`second`

are relatively complex boolean combination of their inputs, that duplicate
the input elements many time. This is all fine and well when the input is just a list
of propositional variable, but when you start combining additions together, you quickly
get an exponential formula size! Because solving a SAT formula itself is non-trivial,
generating and then trying to solve an exponentially large formula quickly becomes infeasible.

The duplication of formula fragments is a very common problem.
The solution is to introduce variable names for common sub-expressions, and ensure
that only variables, but not arbitrarily large formulas are duplicated.
In our case, instead of returning arbitrary formulas in `head`

and `second`

,
you need to introduce fresh propositional variables, constrain them
to be equal to the sub-expression, and return the variables instead of the complex
expressions.
The representation of the result of the addition will be a list of propositional variables,
along with an additional set of constraints that relate them and ensure that these variables compute
the result of the addition.

Take a look at the circuit example from the beginning; this is the exact same technique that is used there. The idea behind introducing intermediate variables is that we want to share previously created constraints by generating alias propositional variables for them. When generating constraints, you may find it helpful to draw the circuits you intend to generate and ensure that you introduce a propositional variable for every wire in the circuit.

Your task is to implement the `adder`

function that generates a adder circuit of arbitrary size:

def adder(n1: List[Formula], n2: List[Formula]): (List[Formula], Set[Formula]) = ???

The `adder`

function takes two numbers encoded with propositional formulas, and
returns a pair. The first element of the pair is a `List[Formula]`

, which, when
evaluated, will give the digits of the result of the addition. The second element is a set of
additional constraints that you create along the way to ensure that the first
element has the correct value.

You will naturally find tests in `ArithmeticSuite.scala`

. If you find that your
tests are running for too long, check that you are not accidentally creating
exponentially large formulas! Some of the tests are actually testing that
`adder`

does not introduce an exponentially large formula. The way to avoid
exponentially large formulas is to introduce fresh propositional variables for
each signal in the circuit, as discussed above.

#### Part 3: Allocating volunteers to tasks

Finally, You can do the allocation of volunteers to tasks. In `Balelec.scala`

, we only
provide the signature of the `schedule`

function that you need to implement. The
signature along with the comments on the source code should be enough to get you
started. If you find yourself lost, you can get some inspiration from the concert
planner you did in part 1, the `schedule`

function works in a similar way.

We did implement two helpers function that use the arithmetic functions that you just implemented. You are not required to use them, but we believe they make the implementation of the scheduling simpler. You are encouraged to read their code and understand how they work.

As in the concert scheduling case, you will have to create certain constraints. For example, you will have to ensure that each task gets exactly the number of volunteers it requires. You are free to introduce as many intermediate functions as required.

Congratulations! You can finally enjoy a cold one at next year's Balélec!