# dac03 shatter

29 %
71 %
Education

Published on January 16, 2008

Author: Regina1

Source: authorstream.com

Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability:  Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability Fadi A. Aloul Igor L. Markov, Karem A. Sakallah The University of Michigan Motivation …:  Motivation … Many powerful SAT solvers are currently available Yet, many EDA instances remain hard to solve Recent work pointed out that breaking symmetries can speed up search E.g. Previous Work:  Previous Work In 1996, Crawford et al.: Laid theoretical foundation for detecting and breaking symmetries in CNF formulas In 2002, Aloul et al.: Extended the framework to handle phase shift symmetries and their composition with permutational symmetries Symmetries in SAT:  Symmetries in SAT Permutations of variables that preserve clauses e.g., symmetries of  = (a + b + c)(d + e + f) include: Slide5:  Symmetries in Search Space SAT Solver Slide6:  Symmetries in Search Space SAT Solver Slide7:  Symmetries in Search Space SAT Solver Symmetry Detection and Breaking Flow:  Symmetry Detection and Breaking Flow CNF instance  = (a+b)(b+c)(c+a) 1 = (ab)(a’b’) 2 = (bc)(b’c’)  = (a+b)(b+c)(c+a) (a’+b)(b’+c) Detect Symmetries Break Symmetries Symmetry Detection and Breaking Flow:  Symmetry Detection and Breaking Flow CNF instance Detect Symmetries Break Symmetries  = (a+b)(b+c)(c+a) 1 = (ab)(a’b’) 2 = (bc)(b’c’)  = (a+b)(b+c)(c+a) (a’+b)(b’+c) Outline:  Outline Basic definitions Symmetry-Breaking Predicate (SBP) construction by Crawford et al. Efficient SBP constructions Experimental results Conclusions Permutations and Generators:  Permutations and Generators Number of symmetries can be exponentially large Represent the group of symmetries implicitly Elementary group theory proves: If redundant generators are avoided A group with N elements can be represented by at most log2(N) generators Generators provide exponential compression of solution space Full Symmetry Breaking:  Full Symmetry Breaking Lex-leader formula [Crawford et al. 96]: Given a group of symmetries defined over totally-ordered variables : For each symmetry , construct a permutation predicate : Image of variable xi under  PP() size:5n clauses0.5n2 + 13.5n literals Linear-Sized PPs:  Linear-Sized PPs PP() size:4n clauses14n literals PP() size:5n clauses0.5n2 + 13.5n literals Linear-Sized Tautology-Free PPs:  Linear-Sized Tautology-Free PPs Variables that map to themselves (i.e. ) lead to: Assume maps to itself: Linear-Sized Tautology-Free PPs:  Linear-Sized Tautology-Free PPs Variables that map to themselves (i.e. ) lead to: Assume maps to itself: Linear-Sized Tautology-Free PPs:  Linear-Sized Tautology-Free PPs Variables that map to themselves (i.e. ) lead to: Assume maps to itself: Linear-Sized Tautology-Free PPs:  Linear-Sized Tautology-Free PPs Variables that map to themselves (i.e. ) lead to: Assume maps to itself: Partial Symmetry-Breaking (1):  Partial Symmetry-Breaking (1) Full symmetry breaking may not speed up search because: Exponential number of symmetries Their SBPs may be redundant Partial symmetry breaking provides a better trade-off Consider first k-variables from each permutation e.g. if k=1 Partial Symmetry-Breaking (1):  Partial Symmetry-Breaking (1) Full symmetry breaking may not speed up search because: Exponential number of symmetries Their SBPs may be redundant Partial symmetry breaking provides a better trade-off Consider first k-variables from each permutation e.g. if k=1 Partial Symmetry-Breaking (2):  Partial Symmetry-Breaking (2) Instead of breaking all symmetries, break only: Generators Generators and their powers Generators and their pair-wise compositions Experimental Results:  Experimental Results % ofbits thatmap tothemselves Generators consisted of cycles of size 2 only Experimental Results*:  Experimental Results* * Break generators only Experimental Results:  Experimental Results Total size of generator-only SBPs using various SBP constructions Experimental Results:  Experimental Results Total search runtimes for all instances when only k bits are considered from each generator (using linear tautology-free construction) Experimental Results:  Experimental Results SBP statistics for various symmetry-breaking candidates using linear tautology-free construction Conclusions:  Conclusions Introduced more efficient CNF constructions of symmetry-breaking predicates Constructions lead to: Empirical speedups Smaller memory requirements Described options for partial symmetry-breaking http://vlsicad.eecs.umich.edu/BK/Slots/shatter/ Thank You!:  Thank You!

 User name: Comment:

## Related presentations

#### 64-bit error patterns in games

December 18, 2018

#### Cisco 400-101 Dumps Questions with Answers

December 18, 2018

#### Best Palace to get Microsoft 70-348 Real Exam Ques...

December 18, 2018

#### Top Search Engine Marketing Course - i Digital Aca...

December 18, 2018

#### No.1 Software Company Lucknow| Build Software For ...

December 18, 2018

#### 70-247 Exam Dumps PDF Questions And Answers

December 18, 2018

## Related pages

### dac03-shatter - Ace Recommendation Platform - 1

AbstractBoolean satisfiability (SAT) solvers have experienced dramatic im-provements in their performance and scalability over the last severalyears [5, 7 ...

### Shatter: Efficient Symmetry-Breaking for Boolean ...

Abstract Boolean satisfiability (SAT) solvers have experienced dramatic im-provements in their performance and scalability over the last several

### dac03-shatter - Ace Recommendation Platform - 1

Shatter: Efficient Symmetry­Breaking for Boolean SatisfiabilityFadi A. AloulIgor L. Markov, ...

### bYTEBoss dac03-shatter

Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability Fadi A. Aloul Igor L. Markov, Karem A. Sakallah The University of Michigan Motivation Many ...

### Shatter: Efficient Symmetry-Breaking for Boolean ...

Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability Fadi A. Aloul Igor L. Markov, Karem A. Sakallah The University of Michigan

### Shatter: Efficient Symmetry-Breaking for Boolean ...

Abstract Boolean satisfiability (SAT) solvers have experienced dramatic im-provements in their performance and scalability over the last several