CSP-to-CSP Translation by Sugar

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_".

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.

This option performs MaxCSP-to-CSP translation.

This option performs WeightedCSP-to-CSP translation.

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

This option enables the translation to linear constraints.

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

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

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

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.

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

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

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

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.

It is isomorphic to CSP output.

• The generated CSP files can be used as Sugar input files.

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
   

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
   

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

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

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

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