The SAT Compiler in Picat 

          Neng-Fa Zhou and Hakan Kjellerstrand 


Picat is a simple, and yet powerful, logic-based multi-paradigm
programming language aimed for general-purpose applications. Picat is
a rule-based language, in which predicates, functions, and actors are
defined with pattern-matching rules. Picat incorporates many
declarative language features for better productivity of software
development, including explicit non-determinism, explicit
unification, functions, list comprehensions, constraints, and
tabling. Picat also provides imperative language constructs, such as
assignments and loops, for programming everyday things. The Picat
implementation, which is based on a well-designed virtual machine and
incorporates a memory manager that garbage-collects and expands the
stacks and data areas when needed, is efficient and scalable. Picat
can be used for not only symbolic computations, which is a
traditional application domain of declarative languages, but also for
scripting and modeling tasks. 

Picat provides facilities for solving combinatorial search problems,
including a common interface with CP, SAT, and MIP solvers, tabling
for dynamic programming, and a module for planning. The common
interface allows for seamless switching from one solver module to
another.

For the sat module, the Picat compiler translates constraints into a
logic formula in the conjunctive normal form (CNF) for the underlying
SAT solver (Lingeling version 587f is used for the competition). Picat
employs the so called log-encoding for compiling domain variables and
constraints.  For a domain with the maximum absolute value n, 
log_2(n) Boolean variables are used. If the domain contains both
negative and positive values, then another Boolean variable is used to
encode the sign. Each combination of values of these Boolean variables
represents a valuation for the domain variable. If there are holes in
the domain, then disequality (!=) constraints are generated in order
to disallow assignments of those hole values to the variable. Equality
and insequality constraints are flattened to two types of primitive
constraints in the form of x>y and x+y=z, which are compiled further
into logic comparators and adders in CNF. For other types of
constraints, clauses are generated in order to disallow conflict
values for the variables. The SAT compiler only performs very limited
optimizations.

The FlatZinc parser is based on the one by Joachim Schimpf.