The Picat-SAT Compiler - PADL'16 Picat-SAT 1 - Outline

Oct 4, 2026

A presentation on compiling constraint satisfaction problems into SAT using Picat. It motivates Picat-SAT by highlighting improved SAT solver performance, the value of SAT as a system backbone, and the scarcity of practical compilers. The talk details Picat constraint modules (domain, arithmetic, boolean, table, global) and explains Booleanization steps for domain variables. It covers sign-and-magnitude log encoding, reified/implicative constraints, and specific arithmetic constraints including addition, multiplication, table, and global constraints, followed by experimental results and conclusions.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages22

Reading Time55 min

AccessFree to download

Outline

Why Picat-SAT?

Picat’s constraint modules

Booleanization of constraints

Experimental results

Conclusion

The Picat-SAT Compiler Neng-Fa Zhou (CUNY Brooklyn College & GC) Joint work with Håkan Kjellerstrand PADL'16 Picat-SAT 1 Outline 􏁮 Why Picat-SAT? 􏁮 Picat’s constraint modules 􏁮 Booleanization of constraints 􏂨 Sign-and-magnitude log encoding of domain variables 􏂨 Primitive, reified, and implicative constraints 􏂨 The addition constraint X+Y = Z 􏂨 The multiplication constraint X*Y = Z 􏂨 Table constraints 􏂨 Global constraints 􏁮 Experimental results 􏁮 Conclusion PADL'16 Picat-SAT 2 Why Picat-SAT? 􏁮 SAT solvers' performance has drastically improved during the past 20 years 􏁮 SAT has become the backbone of many software systems 􏁮 It is viable to build SAT-based CSP solvers 􏁮 There are so many papers but so few compilers 􏂨 Sugar, FznTini , BEE, and meSAT 􏁮 Build a SAT compiler that is solid, efficient, and practically usable PADL'16 Picat-SAT 3 Picat’s Constraint Modules import cp . import sat . import mip . 􏁮 Constraints 􏂨 Domain 􏁮 X :: Domain, X notin Domain 􏂨 Arithmetic 􏁮 (X \#= Y), (X \#!= Y), (X \#> Y), (X \#>= Y),… 􏂨 Boolean 􏁮 (X \#/\ Y), (X \#\/ Y), (X \#<=> Y), (X \#=> Y), (X \#^ Y), (\#~ X), 􏂨 Table 􏁮 table_in (VarTuple,Tuples), table_notin(VarTuple,Tuples) 􏂨 Global 􏁮 all_different(L), element(I, L,V), circuit(L), cumulative(…),… 􏁮 Solver invocation: solve (Options,Vars) PADL'16 Picat-SAT 4 Picat’s Constraint Modules SEND + MORE = MONEY import sat . go => Vars=[S,E,N,D,M,O,R,Y], % generate variables Vars :: 0 . . 9, % define the domains all_different (Vars), % generate constraints S \#!= 0, M \#!= 0, 1000*S+100*E+10*N+D+1000*M+100*O+10*R+E \#= 10000*M+1000*O+100*N+10*E+Y, solve(Vars), % search writeln (Vars) . PADL'16 Picat-SAT 5 Picat’s Constraint Modules Sudoku Board = {{5,3,_ ,_ ,7,_ ,_ ,_ ,_ },{6,_ ,_ ,1,9,5,_ ,_ ,_ }, import sat . {{_8 ,,_9 ,,_8 ,,_ ,,_6 ,,_ ,,_ ,,_6 ,,_3}} ,, {4,_ ,_ ,8,_ ,3,_ ,_ ,1},{7,_ ,_ ,_ ,2,_ ,_ ,_ ,6}, sudoku (Board) => N = Board .len , {{_ ,,_ ,,_ ,,_ ,,_ ,,_ ,,_ ,,_ ,,_}} ,, Vars = Board .vars (), {_ ,_ ,_ ,_ ,_ ,_ ,_ ,_ ,_ }, Vars :: 1 N, {_ ,_ ,_ ,_ ,_ ,_ ,_ ,_ ,_ }} . foreach (Row in Board) all_different (Row) end, foreach (J in 1 N) all_different ([Board[I, J] : I in 1 . .N]) end, M = round( sqrt (N)), foreach (I in 1 . .M . .N-M, J in 1 . .M . .N-M) all_different ([Board[I+K, J+L] : K in 0 . .M-1, L in 0 . .M-1]) end, solve(Vars) . PADL'16 Picat-SAT 6 Booleanization of Constraints 􏁮 Domain variables 􏁮 Primitive, reified, and implicative constraints 􏁮 The addition constraint X+Y = Z 􏁮 The multiplication constraint X*Y = Z 􏁮 Table constraints 􏁮 Global constraints PADL'16 Picat-SAT 7 Encoding Domain Variables 􏁮 Sparse encoding 􏂨 B 􏃳 X = a One Boolean variable is used for each value 􏁮 Order encoding [Sugar, BEE, meSAT] 􏂨 B 􏃳 X ≤ a 􏁮 Log encoding [FznTini] 􏂨 V: [a 1 ,…,an] 􏃳 Each domain variable is encoded as a binary string m = log2 (max(|a 1 |,|an |)) PADL'16 Picat-SAT 8 Log-encoding 􏁮 Pros and Cons 􏂨 Pros: compact, and good for compiling arithmetic constraints 􏂨 Cons: less propagation power 􏁮 Encoding domains that have negative values 􏂨 2’s Complement Representation [FznTini] 􏁮 Only one representation for 0 􏂨 Sign-and-Magnitude Representation [PicatSAT] 􏁮 Efficient codes for Y = abs(X) and Y = -X 􏁮 One extra clause for banning negative zero PADL'16 Picat-SAT 9 Encoding Domain Variables X :: [-2,-1,1,2] 􏃳 􏁮 A Naïve Code 􏁮 An Optimized Code (Using Espresso) PADL'16 Picat-SAT 10

FAQs

Why does the talk propose building a Picat-SAT compiler?

SAT solver performance has improved substantially over the past 20 years and SAT is now a backbone of many software systems. The talk argues it is viable to build SAT-based CSP solvers and notes the gap between many papers and few compilers.

What constraint types does Picat’s constraint module cover?

The outline lists domain constraints, arithmetic constraints, boolean constraints, table constraints, and global constraints. It also shows how to invoke the solver using solve(Options, Vars).

How are domain variables encoded for SAT Booleanization?

It contrasts sparse encoding, order encoding (as used by Sugar/BEE/meSAT), and log encoding (as used by FznTini). For negative domains, it compares 2’s complement representation and sign-and-magnitude representation, including handling for banning negative zero.

Oct 4, 2026

Upload by วิน