Scarab: Program Examples

This page provides some example codes of Scarab.

Home Examples Documents Advanced Usage Tutorial Apps

(Pandiagonal) Latin Square

  • This example is for Latin Square used in CSP Solver Comptitions (CSC2009).

  • Compared to a usual Latin Square (Latin Square in Wikipeida), this one has additional constraints for pandiagonal lines. 

    import jp.kobe_u.scarab._, dsl._

var n: Int = 5
for (i <- 0 until n; j <- 0 until n) int('x (i, j), 1, n)
for (i <- 0 until n) {
  add(alldiff((0 until n).map(j => 'x (i, j))))
  add(alldiff((0 until n).map(j => 'x (j, i))))
  add(alldiff((0 until n).map(j => 'x (j, (i + j) % n))))
  add(alldiff((0 until n).map(j => 'x (j, ((n - 1 + i - j)) % n))))
}

if (find)
  for (i <- 0 until n)
    println((0 until n).map { j => solution.intMap('x (i, j)) }.mkString(" "))

Square Packing

  • Square Packing is a two dimensinal packing problem.
  • Its goal is to pack \(n\) squares each of whose sizes are ranged from 1 to \(n\) into a given (larger sized) container square.
  • The sequences of minimum sized containers for \(n=1,2,3,...,\) is knwon as A005842 of the on-line encyclopedia of integer sequences.
  • Non-overrapping constraint is used to model this problem, which are used in several literature.
    • Kim Marriott, Peter J. Stuckey, Vincent Tam, Weiqing He. Removing Node Overlapping in Graph Layout Using Constrained Optimization. Constraints, 8(2): 143–171, 2003.
    • Takehide Soh, Katsumi Inoue, Naoyuki Tamura, Mutsunori Banbara, Hidetomo Nabeshima. A SAT-based Method for Solving the Two-dimensional Strip Packing Problem. Fundamenta Informaticae, 102(3–4): 467–487, IOS Press, 2010.
  • See also
    • diffn in Global Constraint Catalog.
import jp.kobe_u.scarab._, dsl._

val n = 15; val s =36 

for (i <- 1 to n)  { int('x(i),0,s-i) ; int('y(i),0,s-i) }
for (i <- 1 to n; j <- i+1 to n) 
  add(('x(i)+i <='x(j)) || ('x(j)+j<='x(i)) || ('y(i)+i<='y(j)) || ('y(j)+j<='y(i)))

if (find) println(solution.intMap)

Langford Pairing

Model 1

import jp.kobe_u.scarab._, dsl._

val n = 4

for (i <- 1 to 2*n) int('x(i),1,n)
for (i <- 1 to n) 
  add(Or(for (j <- 1 to 2*n-i-1) yield And(('x(j) === 'x(j+i+1)), ('x(j) === i))))

if(find) println(solution)
  • (Line 7) declare integer variables representing each of \(2n\) positions has which number.

Model 2 (with position variable)

import jp.kobe_u.scarab._, dsl._

val n = 4

for (i <- 1 to n) { 
  int('l(i),1,2*n-i-1)
  int('r(i),1,2*n) 
}

for (i <- 1 to n)  add('l(i) === 'r(i)-i-1)
add(alldiff((1 to n).map(i => 'l(i))))
add(alldiff((1 to n).map(i => 'r(i))))

if(find) println(solution)
  • (Lines 7 to 10) declare integer variables representing each pairs of \(n\) numbers are placed to which positions.

Graph Coloring

  • Graph Coloring (see also Graph Coloring in Wikipedia) is a problem to find a coloring for all nodes of a given graph such that neighbors are colored differently.
  • You can find its instances in URL.
import jp.kobe_u.scarab._, dsl._

val nodes = Seq(1,2,3,4,5)
val edges = Seq((1,2),(1,5),(2,3),(2,4),(3,4),(4,5))
var maxColor = 4;

int('color,1,maxColor)
for (i <- nodes) int('n(i),1,maxColor)
for (i <- nodes) add('n(i) <= 'color)
for ((i,j) <- edges)  add('n(i) !== 'n(j))

while (find('color <= maxColor)) {
  println(solution)
  maxColor -= 1
}

Magic Square

  • Magic Square (see also Magic Square in Wikipedia) is a problem to place \(1\) to \(n^2\) numbers into \(n \times n\) matrix so that sum of each row, sum of each column, sum of each diagonal must be equal to \(\frac{n(n^2+1)}{2}\).
import jp.kobe_u.scarab._, dsl._

val xs = for (i <- 1 to 3; j <- 1 to 3) yield csp.int('x(i,j), 1, 9)
  add(alldiff(xs))

for (i <- 1 to 3)
  add(Sum((1 to 3).map(j => 'x(i,j))) === 15)
for (j <- 1 to 3)
  add(Sum((1 to 3).map(i => 'x(i,j))) === 15)
add(Sum((1 to 3).map(i => 'x(i,i))) === 15)
add(Sum((1 to 3).map(i => 'x(i,4-i))) === 15)

if (find) println(solution)

Alphametic Problem SAT + IS + FUN = TRUE

  • Alphametic Problem (see also Verbal arithmetic in Wikipedia) is one kind of puzzle which represent numbers by alphabets.
  • Goal is to find hidden numbers represented in alphabets by using relations between given words.
  • The following gives an instance SAT + IS + FUN = TRUE (by Prof. Daniel Le Berre) which is originally from an instance CP + IS + FUN = TRUE used in a tutorial of or-tools.
  • SAT + IS + FUN = TRUE is understood as \(S*100 + A*10 + T + I*10 + S + F*100 + U*10 + N = T*1000 + R*100 + U*10 + E\).
import jp.kobe_u.scarab._, dsl._

val base = 10

for (v <- Seq('s,'i,'f,'t)) yield int(v,1,base-1)     // S, I, F and T are not zero
for (v <- Seq('a,'u,'n,'r,'e)) yield int(v,0,base-1)  // others can be zero
for (v <- Seq('c1,'c2,'c3)) yield int(v,0,2)          // carries

add('t + 's + 'n       === 'e + 'c1*base)
add('a + 'i + 'u + 'c1 === 'u + 'c2*base)
add('s +      'f + 'c2 === 'r + 'c3*base)
add(               'c3 === 't)

add(alldiff(Seq('s,'i,'f,'t,'a,'u,'n,'r,'e)))

if (find)  println(solution.intMap)

Open-shop Scheduling

  • Open-shop scheduling is a scheduling problem.
  • The following example uses an instance ``gp03-01’’ given by the paper:
    • (DOI) Guéret, C., & Prins, C. (1999). A new lower bound for the open-shop problem. Annals of Operations Research, 92, 165–183.
  • The following model is given by the paper:
    • (DOI) Naoyuki Tamura, Akiko Taga, Satoshi Kitagawa, Mutsunori Banbara. Compiling finite linear CSP into SAT. Constraints, 14:254–272, 2009.
import jp.kobe_u.scarab._, dsl._

use(new Sat4j("glucose"))

val pt = Seq(
  Seq(661,   6, 333),
  Seq(168, 489, 343),
  Seq(171, 505, 324))

val n = pt.size
val lb = pt.map(_.sum).max
var ub = (0 until n).map(k => (0 until n).map(i => pt(i)((i + k) % n)).max).sum

int('makespan, lb, ub)

for (i <- 0 until n; j <- 0 until n) {
  int('s(i,j), 0, ub)
  add('s(i,j) + pt(i)(j) <= 'makespan)
}
for (i <- 0 until n) {
  for (j <- 0 until n; l <- j+1 until n)
    add('s(i,j) + pt(i)(j) <= 's(i,l) ||
        's(i,l) + pt(i)(l) <= 's(i,j))
}
for (j <- 0 until n) {
  for (i <- 0 until n; k <- i+1 until n)
    add('s(i,j) + pt(i)(j) <= 's(k,j) ||
        's(k,j) + pt(k)(j) <= 's(i,j))
}

while (find('makespan <= ub)) {
  println(solution)
  val end = (for(i <- 0 until n; j <- 0 until n) 
             yield solution.intMap('s(i,j))+pt(i)(j)).max
  ub = end - 1
  println(ub)
}

Colored N Queen

import jp.kobe_u.scarab._, dsl._

val n = args(0).toInt
val c = n

use(new Sat4j("glucose"))

for (i <- 1 to n; color <- 1 to c)
  int('q(i,color), 1, c)

for (color <- 1 to c) {
  add(alldiff((1 to n).map(i => 'q(i,color))))
  add(alldiff((1 to n).map(i => 'q(i,color)+i)))
  add(alldiff((1 to n).map(i => 'q(i,color)-i)))
}

for (i <- 1 to n)
  add(alldiff((1 to c).map(color => 'q(i,color))))

if (find) {
  for (color <- 1 to c) {
    for (row <- 1 to n) {
      var seq: Seq[Int] = Seq.empty
      for (column <- 1 to n)
        if (encoder.decode('q(row,color)) == column)
          seq = seq :+ color
        else
          seq = seq :+ 0
      println(seq.mkString(" "))
    }
    println("-----------------")
  }
}

Author: Takehide Soh

Created: 2019-05-17 金 12:35

Validate