Syntax of Sugar CSP description

Last modified: Mon Jun 23 22:49:32 2008 JST

Introduction

This document explains the syntax of CSP (Constraint Satisfaction Problem) files for Sugar constraint solver.

Preliminaries

Integer ::=
    Digit+ | -Digit+
Digit ::=
    0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
Symbol ::=
    SymbolCharacter+  /* except sequences interpreted as integers */
SymbolCharacter ::=
    /* any character from A-Z a-z 0-9 _ . + - * / % = < > ! & | */
Comment ::=
    ; /* followed by characters until the end of line */

Domain Definitions

Syntax

DomainDefinition ::=
    (domain DomainName LowerBound UpperBound) |
    (domain DomainName (Range+))
DomainName ::=
    Symbol
LowerBound ::=
    Integer
UpperBound ::=
    Integer
Range ::=
    Integer | Integer..Integer

Remarks

Domain names should not be duplicated.

Examples

(domain d0 1000 2000)        ; d0 = { x | 1000 ≤ x ≤ 2000 }
(domain d1 (1..3 5 10..12))  ; d1 = { 1, 2, 3, 5, 10, 11, 12 }

Integer Variable Definitions

Syntax

IntegerVariableDefinition ::=
    (int IntegerVariableName DomainName) |
    (int IntegerVariableName LowerBound UpperBound) |
    (int IntegerVariableName (Range+))
IntegerVariableName ::=
    Symbol

Remarks

Integer variable names should not be duplicated.

Examples

(int x0 d0)               ; x0 ∈ d0
(int x1 1000 2000)        ; x1 ∈ { x | 1000 ≤ x ≤ 2000 }
(int x2 (1..3 5 10..12))  ; x2 ∈ { 1, 2, 3, 5, 10, 11, 12 }

Boolean Variable Definitions

Syntax

BooleanVariableDefinition ::=
    (bool BooleanVariableName)
BooleanVariableName ::=
    Symbol

Remarks

Boolean variable names should not be duplicated.

Examples

(bool p0)

Terms

Syntax

Term ::=
    Integer |
    IntegerVariableName |
    (abs Term) |
    (neg Term) | (- Term) |
    (add Term*) | (+ Term*) |
    (sub Term Term+) | (- Term Term+) |
    (mul Term Term) | (* Term Term) |
    (div Term Term) | (/ Term Term) |
    (mod Term Term) | (% Term Term) |
    (pow Term Term) |
    (min Term Term) |
    (max Term Term) |
    (if LogicalFormula Term Term)

Remarks

At least one argument of mul should be an integer constant. However, some special cases (such as (< (* x y) 0)) are allowed.
The second argument of div and mod should be a positive integer constant.
pow is not supported.

Examples

(- x y z)  ; means x-y-z

Relation Definitions

Syntax

RelationDefinition ::=
    (relation RelationName Arity RelationBody)
RelationName ::=
    Symbol
Arity ::=
    Integer
RelationBody ::=
    (RelationType Tuple*)
RelationType ::=
    supports | conflicts
Tuple ::=
    (Integer+)

Examples

(relation r0 2 (conflicts (0 0) (1 1) (2 2)))

Predicate Definitions

Syntax

PredicateDefinition ::=
    (predicate PredicateHead PredicateBody)
PredicateHead ::=
    (PredicateName Parameter*)
PredicateName ::=
    Symbol
Parameter ::=
    IntegerVariableName
PredicateBody ::=
    LogicalFormula

Remarks

Recursive definitions are not allowed.

Examples

(predicate (p0 x1 x2) (<= x1 (+ x2 1))  ; (p0 x1 x2) ⇔ x1 ≤ x2+1

Constraints

Syntax

Constraint ::=
    LogicalFormula

LogicalFormula ::=
    AtomicFormula |
    (not LogicalFormula) | (! LogicalFormula) |
    (and LogicalFormula*) | (&& LogicalFormula*) |
    (or LogicalFormula*) | (|| LogicalFormula*) |
    (imp LogicalFormula LogicalFormula) | (=> LogicalFormula LogicalFormula) |
    (xor LogicalFormula LogicalFormula) |
    (iff LogicalFormula LogicalFormula)

AtomicFormula ::=
    false | true | BooleanVariableName |
    (eq Term Term) | (= Term Term) |
    (ne Term Term) | (!= Term Term) |
    (le Term Term) | (<= Term Term) |
    (lt Term Term) | (< Term Term) |
    (ge Term Term) | (>= Term Term) |
    (gt Term Term) | (> Term Term) |
    (RelationName Term*) |
    (PredicateName Term*) |
    AllDifferentConstraint |
    WeightedSumConstraint |
    CumulativeConstraint |
    ElementConstraint

Remarks

(and) means true.
(or) means false.

Examples

(or p0 (r0 x4 x5) (>= x0 (+ x0 1))

AllDifferent Constraints

Syntax

AllDifferentConstraint ::=
    (alldifferent Term*) |
    (alldifferent (Term*))

Remarks

See alldifferent constaint in the Global Constraint Catalog.

Examples

(alldifferent (+ x1 1) (+ x2 2) (+ x3 3) (+ x4 4))
(alldifferent ((+ x1 1) (+ x2 2) (+ x3 3) (+ x4 4)))

WeightedSum Constraints

Syntax

WeightedSumConstraint ::=
    (weightedsum (WeightedPair*) ComparisonName Term)
WeightedPair ::=
    (Weight Term)
Weight ::=
    Integer
ComparisionName ::=
    eq | ne | le | lt | ge | gt

Examples

(weightedsum ((1 v0) (2 v1) (-3 v2)) gt 12)  ; means 1*v0+2*v1-3*v3 > 12

Cumulative Constraints

Syntax

CumulativeConstraint ::=
    (cumulative (Task*) Limit) |
Task ::=
    (Origin Duration End Height)
Origin ::=
    Term | nil
Duration ::=
    Term | nil
End ::=
    Term | nil
Height ::=
    Term
Limit ::=
    Term

Remarks

At most one of the origin, duration, and end for each task can be nil.
See cumulative constaint in the Global Constraint Catalog.

Examples

(cumulative ((s0 2 nil 1) (s1 2 nil 1) (s2 2 nil 1) (s3 2 nil 1)) 2)

Element Constraints

Syntax

ElementConstraint ::=
    (element Index (Term+) Value)
Index ::=
    Term
Value ::=
    Term

Remarks

The index value starts from 1.
See element constaint in the Global Constraint Catalog.

Examples

(element i (x1 x2 x3 x4) xi)

Objective Declaration

Syntax

ObjectiveDeclaration ::=
    (objective Goal IntegerVariableName)
Goal ::=
    minimize | maximize

Remarks

Objective declaration should not be duplicated.
MAX-CSP should not include objective declarations.

Examples

(objective minimize x0)  ; The objective is minimizing the value of x0.
(objective maximize x1)  ; The objective is maximizing the value of x1.

CSP

Syntax

CSP ::=
    Statement*

Statement ::=
    DomainDefinition |
    IntegerVariableDefinition |
    BooleanVariableDefinition |
    RelationDefinition |
    PredicateDefinition |
    ObjectiveDeclaration |
    Constaint

Remarks

Definitions should preceed their usage.
Objective variable should be defined before the use in the objective declaration.
Relation names and predicate names should not be duplicated.

Examples

; Magic Square 3 x 3
(int x_1_1 1 9)
(int x_1_2 1 9)
(int x_1_3 1 9)
(int x_2_1 1 9)
(int x_2_2 1 9)
(int x_2_3 1 9)
(int x_3_1 1 9)
(int x_3_2 1 9)
(int x_3_3 1 9)
(alldifferent x_1_1 x_1_2 x_1_3 x_2_1 x_2_2 x_2_3 x_3_1 x_3_2 x_3_3)
(= (+ x_1_1 x_1_2 x_1_3) 15)
(= (+ x_2_1 x_2_2 x_2_3) 15)
(= (+ x_3_1 x_3_2 x_3_3) 15)
(= (+ x_1_1 x_2_1 x_3_1) 15)
(= (+ x_1_2 x_2_2 x_3_2) 15)
(= (+ x_1_3 x_2_3 x_3_3) 15)
(= (+ x_1_1 x_2_2 x_3_3) 15)
(= (+ x_1_3 x_2_2 x_3_1) 15)
; END

; Golomb ruler of 4 marks
(int length 6 7)
(objective minimize length)
(int m_0 0 0)
(int m_1 0 7)
(int m_2 0 7)
(int m_3 0 7)
(< m_0 m_1)
(< m_1 m_2)
(< m_2 m_3)
(<= m_3 length)
(int d_1_0 0 7)
(= d_1_0 (- m_1 m_0))
(int d_2_0 0 7)
(= d_2_0 (- m_2 m_0))
(int d_3_0 0 7)
(= d_3_0 (- m_3 m_0))
(int d_2_1 0 7)
(= d_2_1 (- m_2 m_1))
(int d_3_1 0 7)
(= d_3_1 (- m_3 m_1))
(int d_3_2 0 7)
(= d_3_2 (- m_3 m_2))
(alldifferent d_1_0 d_2_0 d_3_0 d_2_1 d_3_1 d_3_2)
; END

; 4-Queens Problem
(int q_1 1 4)
(int q_2 1 4)
(int q_3 1 4)
(int q_4 1 4)
(alldifferent q_1 q_2 q_3 q_4)
(alldifferent (+ q_1 1) (+ q_2 2) (+ q_3 3) (+ q_4 4))
(alldifferent (- q_1 1) (- q_2 2) (- q_3 3) (- q_4 4))
; END

; Open-Shop Scheduling Problem gp03-01
(int makespan 1000 1509)
(objective minimize makespan)
(int s_0_0 0 1509)
(<= (+ s_0_0 661) makespan)
(int s_0_1 0 1509)
(<= (+ s_0_1 6) makespan)
(int s_0_2 0 1509)
(<= (+ s_0_2 333) makespan)
(int s_1_0 0 1509)
(<= (+ s_1_0 168) makespan)
(int s_1_1 0 1509)
(<= (+ s_1_1 489) makespan)
(int s_1_2 0 1509)
(<= (+ s_1_2 343) makespan)
(int s_2_0 0 1509)
(<= (+ s_2_0 171) makespan)
(int s_2_1 0 1509)
(<= (+ s_2_1 505) makespan)
(int s_2_2 0 1509)
(<= (+ s_2_2 324) makespan)
(or (<= (+ s_0_0 661) s_0_1) (<= (+ s_0_1 6) s_0_0))
(or (<= (+ s_0_0 661) s_0_2) (<= (+ s_0_2 333) s_0_0))
(or (<= (+ s_0_1 6) s_0_2) (<= (+ s_0_2 333) s_0_1))
(or (<= (+ s_1_0 168) s_1_1) (<= (+ s_1_1 489) s_1_0))
(or (<= (+ s_1_0 168) s_1_2) (<= (+ s_1_2 343) s_1_0))
(or (<= (+ s_1_1 489) s_1_2) (<= (+ s_1_2 343) s_1_1))
(or (<= (+ s_2_0 171) s_2_1) (<= (+ s_2_1 505) s_2_0))
(or (<= (+ s_2_0 171) s_2_2) (<= (+ s_2_2 324) s_2_0))
(or (<= (+ s_2_1 505) s_2_2) (<= (+ s_2_2 324) s_2_1))
(or (<= (+ s_0_0 661) s_1_0) (<= (+ s_1_0 168) s_0_0))
(or (<= (+ s_0_0 661) s_2_0) (<= (+ s_2_0 171) s_0_0))
(or (<= (+ s_1_0 168) s_2_0) (<= (+ s_2_0 171) s_1_0))
(or (<= (+ s_0_1 6) s_1_1) (<= (+ s_1_1 489) s_0_1))
(or (<= (+ s_0_1 6) s_2_1) (<= (+ s_2_1 505) s_0_1))
(or (<= (+ s_1_1 489) s_2_1) (<= (+ s_2_1 505) s_1_1))
(or (<= (+ s_0_2 333) s_1_2) (<= (+ s_1_2 343) s_0_2))
(or (<= (+ s_0_2 333) s_2_2) (<= (+ s_2_2 324) s_0_2))
(or (<= (+ s_1_2 343) s_2_2) (<= (+ s_2_2 324) s_1_2))
; END

Naoyuki Tamura