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: The Picat-SAT Compiler PADL 2016 N.F. Zhou and H. Kjellerstrand: Optimizing SAT Encodings for Arithmetic Constraints, CP 2017 N.F. Zhou In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem, CP 2020 We would like to thank Joachim Schimpf for sharing his FlatZinc parser with us and Sanders Hernandez for implementing the SAT interface.