# Scarab: Program Examples

## (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(" "))

• (Lines 1 to 3) import Scarab classes
• (Line 6) declare integer variables
• (Lines 8 to 11) add alldifferenct constraints for each row, column, and diagonal
• (Line 12) print found solution if it exists

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

• (Lines 1 to 3) import Scarab classes
• (Line 7) declare integer variables
• (Lines 8 and 9) add non-overlaping constraints
• (Line 11) print found solution if it exists

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

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
}

• (Lines 5 to 7) declare graph structure.
• (Lines 9 and 10) declare integer variables representing available colors and each node of the given graph.
• (Lines 11 and 12) declare constraints that limit available colors and adjacent nodes have different color.
• (Lines 14 to 17) minimizing number of colors.

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

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)

• (Lines 1 to 3) import Scarab classes
• (Line 5) declare integer variables and puts them to xs
• (Line 6) declare alldiff for the variables
• (Lines 8 and 11) add constraints such that the sum for each row and column become 15
• (Line 12 and 13) add constraints such that the sum for each main diagonal become 15
• (Line 15) print found solution if it exists

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

if (find)  println(solution.intMap)

• (Lines 11 to 14) constraint model considering each digit and carry, which takes around 1 second;)

## Open-shop Scheduling

• Open-shop scheduling is a scheduling problem.
• The following example uses an instance gp03-01’’ given by the paper:
• (DOI) Gué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)
}
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)
}

• (Lines 1 to 3) import Scarab classes
• (Lines 7 to 10) declare an instance
• (Lines 12 to 14) compute size, lower and upper bounds of the instance
• (Line 16) declares an integer variable representing current makespan
• (Lines 18 to 21) forces all operations are ended before makespan
• (Lines 22 to 26) forces for operations in the same job do not overlap each other
• (Lines 27 to 31) forces for operations sharing same resource do not overlap each other
• (Lines 33 to 38) coumputes optimum solution

## 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) {
}

for (i <- 1 to n)

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("-----------------")
}
}

• (Lines 1 to 3) import Scarab classes
• (Lines 5 to 6) size is given from command line
• (Lines 8) declares the use of Sat4j of Glucose setting.
• (Lines 10 to 11) declares integer variables representing queens
• (Lines 13 to 17) representing N-Queen constraints for each color
• (Lines 19 to 20) forces that Queens of each color do no overlap
• (Lines 22 to 35) compute solutions and show the obtained placement

Created: 2019-05-17 金 12:35

Validate