CSP-to-CSP Translation by Sugar

Table of Contents

What's New

  • 2013-02-15 Fri
    • First public release

Introduction

This document explains the usage of CSP-to-CSP translation function of Sugar.

trans.png

Download

  • trans.zip (sample input and output files, and trans.pro program)

Usage

Java command

java -jar sugar-v2-1-2.jar -option options -to csp output.csp input.csp

  • The above command generates the output in Sugar CSP format.
  • By replacing -to csp option with -to prolog, Prolog format output is generated.
  • The options string is a list of option settings separated by commas (,). Option setting is either an option name or an option name preceded with "no_".

Example

$ java -jar sugar-v2-1-2.jar -option no_norm,no_simp,no_reduce,no_decomp,no_hints -to csp output.csp input.csp

Sugar command

The next command can be used to get the same result.

sugar -option options -translate format -output output.csp input.csp

  • The format is either csp or prolog.

Example

$ sugar -option no_norm,no_simp,no_reduce,no_decomp,no_hints -translate csp -output output.csp input.csp

Translations

The following translations are always performed.

  • Domain names are replaced with their definitions.
    For example,
    (domain d0 1 9)
    (int x d0)
    

    is converted to the following.

    (int x ((1 9)))
    
  • Predicates are expanded with their definitions.
    For example,
    (predicate (p0 x1 x2) (<= x1 (+ x2 1)))
    (p0 (+ x 1) 2)
    

    is converted to the following at first, and further translations are performed.

    (<= (+ x 1) (+ 2 1))
    
  • Each constraint is converted to clausal form when linearize option is set. Each clause consists of the followings or their nagations.
    • Boolean variable
    • Relation
    • Linear comparison (eq, ne, le)
    • General comparison (when it is not linearized)
    • Global constraint (when it is not decomposed)

Optional translations

max (default off)

This option performs MaxCSP-to-CSP translation.

weighted (default off)

This option performs WeightedCSP-to-CSP translation.

peephole, peep (default on)

This option performs peephole optimization for some expressions, such as x ⋅ y ≤ 0 and abs(x) ≤ y.

linearize, linear (default on)

This option enables the translation to linear constraints.

propagation, prop (default on)

This option performs constraint propagation to reduce domains of integer variables and remove redundant constraints.

normalize_linearsum, norm (default on)

This option performs conversion of linear comparisons (eq, ne, le, lt, ge, gt) to linear comparisons of "le" or "ge". When this option is disabled and linearize option is set, linear comparisons are converted to "eq", "ne", "le", or "ge".

simplify_clauses, simp (default on)

This option performs Tseitin translation so that each clause contains at most one non-simple literal. The followings are simple literals.

  • Boolean variable or its negation
  • Linear comparison x≤ a or x≥ a

reduce_arity, reduce (default on)

This option reduces the arity of linear comparisons by introducing new integer variables.

  • When "arity=n" is specified, "n" is used as the maximum arity.

decompose, decomp (default on)

This option performs decomposition of all global constraints. The option for each global constraint is as follows.

  • decompose_alldifferent, decomp_alldiff
  • decompose_weightedsum, decomp_wsum
  • decompose_cumulative, decomp_cumul
  • decompose_element, decomp_elem
  • decompose_disjunctive, decomp_disj
  • decompose_lex_less, decomp_lex_less
  • decompose_lex_lesseq, decomp_lex_lesseq
  • decompose_nvalue, decomp_nvalue
  • decompose_global_cardinality, decomp_gc
  • decompose_global_cardinality_with_costs, decomp_gcc
  • decompose_count, decomp_count

replace_arguments, replace_args (default off)

This option replaces the expressions used as the arguments of alldifferent constraints to integer variables.

hints (default on)

This option adds pigeon-hole clauses (Hall clauses) to alldifferent constraints.

Output

CSP output

The following explains the format of the output under linear, prop, no_norm, no_simp, no_reduce, no_decomp, no_hints settings. Only the differences from the original Sugar syntax are described.

Integer Variable Definitions

IntegerVariableDefinition ::=
    (int IntegerVariableName (Range+))
Range ::=
    (Integer Integer)

Boolean Variable Definitions

BooleanVariableDefinition ::=
    (bool BooleanVariableName)
  • This is same with the original syntax definition.

Relation Definitions

RelationDefinition ::=
    (relation RelationName Arity RelationBody)
  • This is same with the original syntax definition.

Predicate Definitions

  • No predicate definitions are included in the output.

Constraints

Constraint ::=
    Clause

Clause ::=
    Literal |
    (or Literal+)

Literal ::=
    BooleanVariableName | (not BooleanVariableName) |
    (RelationName Term*) | (not (RelationName Term*)) |
    LinearComparison |
    GlobalConstraint | (not GlobalConstraint)

LinearCompariosn ::=
    (wsum (WeightedPair*) Comparison Integer)
WeightedPair ::=
    (Integer IntegerVariableName)
Comparison ::=
    eq | ne | le

GobalConstraint ::=
    AllDifferentConstraint |
    WeightedSumConstraint |
    CumulativeConstraint |
    ElementConstraint |
    DisjunctiveConstraint |
    Lex_lessConstraint |
    Lex_lesseqConstraint |
    NvalueConstraint |
    Global_cardinalityConstraint |
    Global_cardinality_with_costsConstraint |
    CountConstraint
  • When translated from XCSP input, the arguments of relations are only integer variables or integer constants.
  • When translated from XCSP input, the arguments of global constraints are only integer variables or integer constants.
  • When normalize_linearsum option is specified, Comparison is always le.

CSP

CSP ::=
    false |
    IntegerVariableDefinition*
    BooleanVariableDefinition*
    RelationDefinition*
    ObjectiveDeclaration?
    Constraint*

Prolog output

It is isomorphic to CSP output.

Example

The following example.csp file is used.

(int x 1 9)
(int y (2 3 5 8 9))
(int z ((1 3) 5 (7 9)))
(int w -1000 1000)
(bool p)
(bool q)
(bool r)
(relation r 2 (conflicts (1 2) (3 4)))
(imp p (imp q r))
(iff (r x y) (r y x))
(> (+ x y) 10)
(imp (= x 9) (and p q (= z 1)))
(or (>= (+ x y) 10) (>= (+ y z) 10))
(>= (+ w (abs w) x y z) 100)
(alldifferent x y z)

CSP to CSP

Optionslinearpropnormsimpreducedecomphints
example-xxxxxxx.csp-------
example-Lxxxxxx.cspY------
example-LPxxxxx.cspYY-----
example-LPNxxxx.cspYYY----
example-LPNSxxx.cspYYYY---
example-LPNSRxx.cspYYYYY--
example-LPNSRDx.cspYYYYYY-
example-LPNSRDH.cspYYYYYYY
  • The generated CSP files can be used as Sugar input files.

CSP to Prolog

Optionslinearpropnormsimpreducedecomphints
example-xxxxxxx.pro-------
example-Lxxxxxx.proY------
example-LPxxxxx.proYY-----
example-LPNxxxx.proYYY----
example-LPNSxxx.proYYYY---
example-LPNSRxx.proYYYYY--
example-LPNSRDx.proYYYYYY-
example-LPNSRDH.proYYYYYYY

Writing Prolog program to generate customized output

It seems a good approach to write a Prolog program which reads Prolog list format output and generates desired output.

trans.pro is such a small Prolog program runnable under SWI-Prolog. trans.sh is a shell script to run the program.

$ ./trans.sh example-LPxxxxx.pro

The following is an output of trans.pro program for example-LPxxxxx.pro.

int(x,'.'(range(2,9),[])).
int(y,'.'(range(2,3),'.'(range(5,5),'.'(range(8,9),[])))).
int(z,'.'(range(1,3),'.'(range(5,5),'.'(range(7,9),[])))).
int(w,'.'(range(-927,1000),[])).
int('$I1','.'(range(0,1000),[])).
bool(p).
bool(q).
bool(r).
bool('$B1').
relation(r,2,conflicts,'.'('.'(1,'.'(2,[])),'.'('.'(3,'.'(4,[])),[]))).
constraint(1).
constraint_elem(1,not(p)).
constraint_elem(1,not(q)).
constraint_elem(1,r).
constraint(2).
constraint_elem(2,not(rel(r,'.'(x,'.'(y,[]))))).
constraint_elem(2,rel(r,'.'(y,'.'(x,[])))).
constraint(3).
constraint_elem(3,rel(r,'.'(x,'.'(y,[])))).
constraint_elem(3,not(rel(r,'.'(y,'.'(x,[]))))).
constraint(4).
constraint_elem(4,rel(wsum,'.'('.'('.'(1,'.'(x,[])),'.'('.'(1,'.'(y,[])),[])),'.'(ge,'.'(11,[]))))).
constraint(5).
constraint_elem(5,rel(wsum,'.'('.'('.'(1,'.'(x,[])),[]),'.'(ne,'.'(9,[]))))).
constraint_elem(5,'$B1').
constraint(6).
constraint_elem(6,p).
constraint_elem(6,not('$B1')).
constraint(7).
constraint_elem(7,q).
constraint_elem(7,not('$B1')).
constraint(8).
constraint_elem(8,rel(wsum,'.'('.'('.'(1,'.'(z,[])),[]),'.'(eq,'.'(1,[]))))).
constraint_elem(8,not('$B1')).
constraint(9).
constraint_elem(9,rel(wsum,'.'('.'('.'(1,'.'(x,[])),'.'('.'(1,'.'(y,[])),[])),'.'(ge,'.'(10,[]))))).
constraint_elem(9,rel(wsum,'.'('.'('.'(1,'.'(y,[])),'.'('.'(1,'.'(z,[])),[])),'.'(ge,'.'(10,[]))))).
constraint(10).
constraint_elem(10,rel(wsum,'.'('.'('.'(1,'.'('$I1',[])),'.'('.'(-1,'.'(w,[])),[])),'.'(ge,'.'(0,[]))))).
constraint(11).
constraint_elem(11,rel(wsum,'.'('.'('.'(1,'.'('$I1',[])),'.'('.'(1,'.'(w,[])),[])),'.'(ge,'.'(0,[]))))).
constraint(12).
constraint_elem(12,wsum('.'(mul(1,'$I1'),'.'(mul(-1,w),[])),le,0)).
constraint_elem(12,wsum('.'(mul(1,'$I1'),'.'(mul(1,w),[])),le,0)).
constraint(13).
constraint_elem(13,rel(wsum,'.'('.'('.'(1,'.'('$I1',[])),'.'('.'(1,'.'(w,[])),'.'('.'(1,'.'(x,[])),'.'('.'(1,'.'(y,[])),'.'('.'(1,'.'(z,[])),[]))))),'.'(ge,'.'(100,[]))))).
constraint(14).
constraint_elem(14,alldifferent('.'(x,'.'(y,'.'(z,[]))))).
  • List [x1,x2,...,xn] is represented by a nested term '.'(x1, '.'(x2, …, '.'(xn, []) …)).

Translation Hooks

You can add hooks of calling your conversion program to the translation procedure.

Solving CSP with your conversion program

  1. Write your conversion program implementing jp.kobe_u.sugar.hook.ConverterHook interface. See ExampleHook.java as an example program.
  2. Compile
    $ javac -cp sugar-v2-1-2.jar ExampleHook.java
    
  3. Run
    $ sugar -jar .:sugar-v2-1-2.jar -conversionHooks ExampleHook example2.csp
    

Translating CSP with your conversion program

  1. Write your conversion program implementing jp.kobe_u.sugar.hook.ConverterHook interface. See ExampleHook.java as an example program.
  2. Compile
    $ javac -cp sugar-v2-1-2.jar ExampleHook.java
    
  3. Run
    $ java -cp .:sugar-v2-1-2.jar jp.kobe_u.sugar.SugarMain -conversionHooks ExampleHook
      -option no_norm,no_simp,decomp -to csp example2out.csp example2.csp
    

    Alternatively way

    $ sugar -jar .:sugar-v2-1-2.jar -conversionHooks ExampleHook
      -option no_norm,no_simp,decomp -translate csp -output example2out.csp example2.csp
    

Example input

(int x1 0 99)
(int x2 0 99)
(int x3 0 99)
(int y1 1 3)
(int y2 1 3)
(int y3 1 3)
(= x1 myconstant)
(mypredicate x1 x2 x3)
(alldifferent y1 y2 y3)

Example output

; File generated by sugar.Output
(int x1 ((55 55)))
(int x2 ((56 98)))
(int x3 ((57 99)))
(int y1 ((1 3)))
(int y2 ((1 3)))
(int y3 ((1 3)))
; (eq x1 myconstant)
(wsum ((1 x1)) eq 55)
; (mypredicate x1 x2 x3)
(wsum ((1 x1) (-1 x2)) le -1)
(wsum ((1 x2) (-1 x3)) le -1)
; (alldifferent y1 y2 y3)
(or (wsum ((1 y1)) ge 3) (wsum ((1 y2)) ge 3) (wsum ((1 y3)) ge 3))
(or (wsum ((1 y1)) le 1) (wsum ((1 y2)) le 1) (wsum ((1 y3)) le 1))
(or (wsum ((1 y1)) eq 1) (wsum ((1 y2)) eq 1) (wsum ((1 y3)) eq 1))
(or (wsum ((1 y1)) eq 2) (wsum ((1 y2)) eq 2) (wsum ((1 y3)) eq 2))
(or (wsum ((1 y1)) eq 3) (wsum ((1 y2)) eq 3) (wsum ((1 y3)) eq 3))

Example program

import java.util.ArrayList;
import java.util.List;

import jp.kobe_u.sugar.SugarException;
import jp.kobe_u.sugar.converter.Converter;
import jp.kobe_u.sugar.csp.Clause;
import jp.kobe_u.sugar.csp.IntegerDomain;
import jp.kobe_u.sugar.expression.Expression;
import jp.kobe_u.sugar.expression.Sequence;
import jp.kobe_u.sugar.hook.ConverterHook;

/**
 * @author Naoyuki Tamura (tamura@kobe-u.ac.jp)
 * 
 */
public class ExampleHook implements ConverterHook {
    private static Expression MyConstant = Expression.create("myconstant");
    private static Expression MyPredicate = Expression.create("mypredicate");

    @Override
    public Expression convertFunction(Converter converter, Expression x)
            throws SugarException {
        if (x.equals(MyConstant)) {
            // myconstant --> 55
            Expression z = Expression.create(55);
            return z;
        }
        return x;
    }

    @Override
    public Expression convertConstraint(Converter converter, Expression x,
            boolean negative, List<Clause> clauses) throws SugarException {
        if (x.isSequence(MyPredicate)) {
            // (mypredicate x1 x2 x3 ...) --> (and (< x1 x2) (< x2 x3) ...)
            Sequence seq = (Sequence) x;
            List<Expression> xs = new ArrayList<Expression>();
            xs.add(Expression.AND);
            for (int i = 1; i < seq.length() - 1; i++)
                xs.add(seq.get(i).lt(seq.get(i + 1)));
            Expression z = Expression.create(xs);
            return z;
        } else if (x.isSequence(Expression.ALLDIFFERENT)) {
            return convertAlldifferent(converter, (Sequence)x, negative, clauses);
        }
        return x;
    }

    private Expression convertAlldifferent(Converter converter, Sequence seq,
            boolean negative, List<Clause> clauses) throws SugarException {
        // Convert alldifferent by default
        Expression z = converter.convertGlobal(seq, negative, clauses);
        // Get arguments
        Expression[] args;
        if (seq.length() == 2 && seq.get(1).isSequence()) {
            args = ((Sequence) seq.get(1)).getExpressions();
        } else {
            args = new Expression[seq.length() - 1];
            for (int i = 1; i < seq.length(); i++)
                args[i - 1] = seq.get(i);
        }
        int n = args.length;
        // Calculate bounds of the arguments
        int lb = Integer.MAX_VALUE;
        int ub = Integer.MIN_VALUE;
        for (Expression x : args) {
            IntegerDomain d = converter.convertFormula(x).getDomain();
            lb = Math.min(lb, d.getLowerBound());
            ub = Math.max(ub, d.getUpperBound());
        }
        // Add At-Least-One clause when it is a permutation
        if (n == ub - lb + 1) {
            for (int value = lb; value <= ub; value++) {
                List<Expression> alo = new ArrayList<Expression>();
                alo.add(Expression.OR);
                for (Expression x : args) {
                    alo.add(x.eq(value));
                }
                if (z == null)
                    z = Expression.create(alo);
                else
                    z = z.and(Expression.create(alo));
            }
        }
        return z;
    }
}

Output Hooks

You can add hook of calling your output program.

Ouptut with your conversion program

  1. Write your output program implementing jp.kobe_u.sugar.OutputInterface interface.
  2. Compile
    $ javac -cp sugar-v2-1-2.jar Output.java
    
  3. Run
    $ java -cp .:sugar-v2-1-2.jar jp.kobe_u.sugar.SugarMain -outputHook Output
      -option no_norm,no_simp,decomp -to csp example2out.csp example2.csp
    

    Alternatively way

    $ sugar -jar .:sugar-v2-1-2.jar -outputHook Output
      -option no_norm,no_simp,decomp -translate csp -output example2out.csp example2.csp
    

Date: 2013-12-24 23:57:19 JST

Author: Naoyuki Tamura

Org version 7.8.02 with Emacs version 23

Validate XHTML 1.0