LARA

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.

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:

http://www.scala-lang.org/api/current/index.html

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.

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.

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.

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 Formulas: && (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.

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!

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.

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.

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.

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) && ???

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.

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).

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.

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)).

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.

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!