The Picat-SAT Compiler

4 years 3 months ago
The Picat-SAT Compiler
SAT has become the backbone of many software systems. In order to make full use of the power of SAT solvers, a SAT compiler must encode domain variables and constraints into an efficient SAT formula. Despite many proposals for SAT encodings, there are few working SAT compilers. This paper presents Picat-SAT, the SAT compiler in the Picat system. Picat-SAT employs the sign-and-magnitude log encoding for domain variables. Log-encoding for constraints resembles the binary representation of numbers used in computer hardware, and many algorithms and optimization opportunities have been exploited by hardware design systems. This paper gives the encoding algorithms for constraints, and attempts to experimentally justify the choices of the algorithms for the addition and multiplication constraints. This paper also presents preliminary, but quite encouraging, experimental results.
Neng-Fa Zhou, Håkan Kjellerstrand
Added 08 Apr 2016
Updated 08 Apr 2016
Type Journal
Year 2016
Where PADL
Authors Neng-Fa Zhou, Håkan Kjellerstrand
Comments (0)