ppt

```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.
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
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
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
```