Report

Programming with Boolean Satisfaction Michael Codish Department of Computer Science Ben Gurion University Beer-Sheva , Israel Joint work with: Vitaly Lagoon, Amit Metodi & Peter Stuckey CP meets CAV - 2012 I. Its all about solving hard problems Solving hard problems (Programming) Problem (hard) Theory tells us • Look for approximations • Look for easier sub-classes direct Practice tells us • Apply heuristics • Try to be clever Solution Theory also tells us • It is all equivalent to SAT Solving hard problems via SAT encodings Problem (hard) hype! decoding CNF sat solving direct Solution encoding SAT ’ing Assignment Improved techniques Solving hard problems via SAT encodings encoding direct hype! (hard) Many success stories Solution decoding CNF sat solving Problem SAT solvers are getting stronger by the day SAT ’ing Assignm. Emerging tools like “Sugar”, “Bee”, and others Example: encoding Sudoku cells rows columns boxes “unit clauses” At least = cell (i,j) contains value k At most Example: solving Sudoku SAT Solver solution We Can Solve Also More Interesting Problems But, there are also less interesting problems that we cannot solve Eternity II: 2 million $ prize unclaimed 17 challenge: prize unclaimed $ 3 months ago ! (Steinbach & Posthoff) We will always have the phase transition How hard interesting problem instances Problem size We seek better encodings so that our preferred problem instances will be solvable Solving hard problems tedious; often repetitive; generatingvia SAT encodings millions of clauses This was a great talk…. (a few years ago) Problem encoding CNF direct hype! sat solving (hard) Solution decoding SAT ’ing Assignm. “and i have some conclusions” I have been doing this for the past few years Me: primarily for applications of termination analysis II. encoding direct hype! (hard) Solution decoding Satisfaction (CP meets CAV 2012) CNF sat solving Problem Programming with Boolean SAT ’ing Assignm. II. Problem (hard) encoding Programming with Boolean Satisfaction CNF Q. What makes a program work better? higher-level languages compilers & tools (p.e.) Data Structures / algorithms hardware Q. What makes a program work better? unit propagation /arc consistency default value (1 or 0) clause / variable ordering Choice of SAT solver hardware Q. What makes a program work better? higher-level languages compilers & tools (p.e.) Data Structures / algorithms hardware Outline Introduction: Solving hard problems via SAT Focus on programming with SAT The need for higher-level languages Higher low-level Language (the basics for) A Compiler to CNF Example: Model Based Diagnosis Representing Finite Domain Integers Example: Magic Labels Conclusion higher-level language ? Problem (hard) Problem (hard) modeling encoding Constraint Model CNF encoding CNF higher-level language Finite Domain & Boolean Constraints Subset of FlatZinc The compiler Problem (hard) modeling Constraint Model encoding CNF Example: encoding Sudoku Problem (hard) modeling Constraint Model encoding CNF user Problem (hard) modeling compiler Constraint Model encoding The CNF per constraint is small & gives context for the bits (word-level) The CNF is large & we have no context for the bits (bit-level) CNF Problem (hard) modeling compiler Constraint Model Tools such: SatELite, ReVivAl Based on Unit Propagation and Resolution. remove redundant variable X if the CNF implies X=Y, X= -Y, X=0, X=1 CryptoMiniSAT tries to add “xor clauses” encoding CNF simplification user smaller CNF user (hard) modeling apply constraint simplification (partial evaluation remove redundant variable X if the Constraint implies X=Y, X= -Y, X=0, X=1 Constraint Model simplification Problem compiler encoding CNF smaller CNF smaller Constraint Model bit-level techniques even smaller CNF such x can be removed from all constraints. of the form X=L where L is a constant or a literal: X=Y, X= -Y, X=0, X=1 Implemented: complete / adhoc equi-propagation Constraint Model simplification Equi-propagation is the process of inferring equations implied by a “few” constraints. smaller Constraint Model constraint simplification is word-level (looking at the bits) Simplify M= M’ = Constraint ( C1, φ1 ) Constraint ( C2, φ2 ) Constraint ( C3, φ3 ) … Boolean techniques (equi-propagation) CSP techniques (partial evaluation) Constraint ( C1, φ1 ) Constraint ( Cn, φn ) Constraint ( C2, φ2 ) Constraint ( C’3, φ‘3 ) … Constraint ( C’n, φ’n ) Equi-propagation for Optimized SAT Encoding; Amit Metodi, Michael Codish, Vitaly Lagoon and Peter Stuckey; CP 2011 Outline Introduction: Solving hard problems via SAT Focus on programming with SAT The need for higher-level languages Higher low-level Language (the basics for) A Compiler to CNF Example: Model Based Diagnosis Representing Finite Domain Integers Example: Magic Labels Conclusion Example: Model Based Diagnosis 1 A 0 B 1 C Full Adder Z1 D 0 Z3 Z2 E 0 1 Diagnoses: min-cardinality Modeling MBD: introduce health variables 1 A 0 B 1 C X1 Z1 A1 D 0 X2 H1 H2 Z2 A2 H4 Z3 O1 E 0 H5 H3 H -H sum( [ -H1, -H2, -H3, -H4, -H5 ] ) ≤ K Modeling MBD: introduce health variables 1 A 0 B 1 C X1 Z1 A1 H3 D 0 X2 H1 H2 Z2 A2 H4 Z3 O1 E 0 H5 green means “healthy” sum( [ -H1, -H2, -H3, -H4, -H5 ] ) ≤ 1 encoding to SAT is Not competitive straighforward with other MBD standard: tools Smith 2005 Simplify the encoding 1 A 0 B 1 C X1 Z1 A1 D 0 X2 H1 H2 Z3 A2 H4 Z2 O1 H5 H3 equi-propagation Z2=-H3 partial evaluation 1 -H3 0 E 0 1 1 0 0 H3 A1 -H3 gray means "melted” 0 Z2 Simplify the encoding - I 1 A 0 B 1 C X1 H1 A1 D 0 X2 H1 H2 Z3 A2 H4 -H3 O1 H5 H3 equi-propagation Z2=-H partial evaluation 1 -H3 0 E 0 1 1 0 0 H3 A1 -H3 gray means "melted” 0 Z2 Simplify the encoding - I 1 A 0 B 1 C X1 H1 A1 D 0 X2 H1 H2 Z3 A2 H4 -H3 O1 H5 H3 equi-propagation Z2=-H partial evaluation 1 -H3 0 E 0 1 1 0 0 H3 A1 -H3 gray means "melted” 0 Z2 Simplify the encoding - II 1 A 0 B 1 C X1 H1 A1 H3 D 0 X2 H1 H2 -H3 A2 H4 Z3 O1 E 0 H5 dominator claim: A minimal cardinality diagnosis will always indicate at most one unhealthy gate per “cone”. And wlog it is the “dominator” Simplify the encoding - II 1 A 0 B 1 C X1 H1 A1 H3 D 0 X2 H1 H2 -H3=0 A2 H4 Z3 O1 E 0 H5 green means “healthy” sum( [ -H1, -H2, 0, 0, -H5 ] ) ≤ K Simplify the encoding - II 1 A 0 B 1 C X1 H1 X2 H1 A1 H2 -H3=0 A2 H4 H1 H3 No SAT solving; sum( [ -H1, -H2, Diagnostics (min-cardinality) found by: preprocessing(cones) partial evaluation equi-propagation D 0 H1=H2 H1=-H5 O1 E 0 H5 -H5 ] ) ≤ K sum( [ -H1, -H2, H1 ] ) ≤ K sum( [ -H1, -H1, H1 ] ) ≤ K Compiling Model-Based Diagnosis to Boolean Satisfaction; Amit Metodi, Roni Stern, Meir Kalech, Michael Codish; AAAI 2012 (to appear) very good experimental results. overtakes all current MBD systems finds (for the first time) minimal cardinality diagnosis for the entire standard benchmarks Outline Introduction: Solving hard problems via SAT Focus on programming with SAT The need for higher-level languages Higher low-level Language (the basics for) A Compiler to CNF Example: Model Based Diagnosis Representing Finite Domain Integers Example: Magic Labels Conclusion Modeling Finite Domain CSP representing numbers (integers) Binary Unary integer variable X with domain {0,…,d} is represented in integer variable X with domain {0,…,d} is represented in bits bits Direct encoding Order encoding xi ↔ (X = i) xi ↔ (X ≥ i) (X = 3) = [0,0,0,1,0,0] (X = 3) = [1,1,1,0,0] Why Order Encoding ? good for representing ranges (Sugar) X X≥i 1 0 i j X<j good for arbitrary sets (Bee) X uv b=c e=f=g a b c d e f g i Why Order Encoding ? Lots of equi-propagation order encoding The Encoding to SAT needs NO Clauses. It is obtained by unification Why Order Encoding ? Lots of equi-propagation Implementing Equi-propagation 1. Using BDD’s. • Can be prohibitive for global constraints. • Complete 2. Ad-Hoc rules (per constraint type) • Fast, precise in practice • Incomplete 3. Using SAT (on small groups of constraints) • Not too slow • Complete Ben-Gurion Equi-propagation Encoder BEE compiler Problem (hard) modeling Constraint Model encoding CNF Constraint Model choice of representation (default is order encoding) partial evaluation equi-propagation decomposition bit-blasting constraint simplification encoding CNF Constraint ( C1, φ1 ) standard techniques (but encoding technique may differ after simplification) Example: Magic Labels (VMTL) v4 e34 v3 e23 v2 e13 v1 e12 6v4 8 1v3 2 v52 3 7 4 v1 simplifying sum constraints bound propagation ? A & B take values {6,7,8} is it a CSP thing? no. it is equi-propagation simplifying sum constraints e.p. p.e. e.p . back to the VMTL example v4 e34 v3 e23 v2 e13 v1 e12 6v4 8 1v3 2 v52 3 7 4 v1 VMTL: Simplifying Constraints could take values 6,7,8 could take values 6,8 Example: Magic Labels (VMTL) 909 clauses 136 Bits 298 clauses 49 Bits BIBD Graph Crossing MAS Kakuro Protein folding N-Queens System Diagnostic Magic Square SCM / MCM QCP / Sudoku Nonograms Compiling Finite Domain Constraints to SAT with Bee (tool paper & release); Amit Metodi and Michael Codish; ICLP 2012 Implementation Currently we use CryptoMiniSAT (or MiniSAT) The compiler is written in Prolog (SWI) (equating Boolean variables using unification) SAT, BDD and Adhoc rules to implement E.P. Where now? • applications • implementation • complete equi-propagation (on chunks) • how to implement it • how to decide where to apply it Conclusions New Emerging Paradigm where we program with SAT (or SMT) solvers; High”er-level (constraint based) language to aid in the encoding lets us focus on the modeling The notion of E.P. captures many standard CSP techniques and more. Making the CNF smaller is not the real goal; It is more about restricting the search space by identifying equalities that must hold