CHANGES of Sugar

This document describes the major changes of Sugar (A SAT-based Constraint Solver).

• Converter is modified to support SugarLoader and XCSPLoader of Copris.
• Inequalities are used to introduce aux variables in inequalties.

• GCNF and GWCNF output

  sugar -n -o gcnf -sat output.gcnf input.csp
  

• New option in CSP-to-CSP translator

  sugar -o arity=3 -translate csp -output output.csp input.csp
  

• SMT output (QF_LIA) in CSP-to-CSP translator

  sugar -o no_norm,no_reduce -translate smt -output output.smt2 input.csp
  

• Use cache in Tseitin transformation. Cache size can be changed by "-o simp_cache=2000" (default 1000).

• Bug fix when the given CSP is trivially unsatisfiable.
• Code refactoring

• Package name space is changed to jp.kobe_u.sugar from jp.ac.kobe_u.cs.sugar.
• Refactoring code of the Converter program
• Refactoring code of the Encoder program
• CSP-to-CSP translation mode is added
  • See http://bach.istc.kobe-u.ac.jp/sugar/docs/translator.html
• Bug fix for negative relations

• Support for Scala interface named Copris (Constraint Programming in Scala) is added (see http://bach.istc.kobe-u.ac.jp/copris/).

• UTF-8 code support for CSP files
• Incremental search mode for optimization problems
• Show values of bool variables
• Debug option is added
• Following global constraints are added
  • disjunctive
  • lex_less
  • lex_lesseq
  • nvalue
  • global_cardinality
  • global_cardinality_with_costs
  • count
• Performance improvements
  • Expressions are encoded from smaller domain size variables
  • Smaller domain expressions are directly encoded withou introducing new variables

• Global constraint "allDifferent" is renamed to "alldifferent".
• Global constraint "weightedSum" is renamed to "weightedsum".
• "alldifferent" constraint is modified to accept a single list argument.
  • Both "(alldifferent x1 x2 x3)" and "(alldifferent (x1 x2 x3))" can be used.
• Maximization is supported.
• Bug fix for picosat support.