PicatSAT: A 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 (the Kissat solver 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. Picat-SAT
flattens intensional constraints into primitive ones. It performs
numerous optimizations, both in the phase of breaking constraints into
primitive ones and in the phase of compiling primitive constraints
into adders and comparators. Details can be found in:

N.F. Zhou and H. Kjellerstrand:
Optimizing SAT Encodings for Arithmetic Constraints,
CP 2017

We would like to thank Joachim Schimpf for sharing his FlatZinc parser
with us.