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