advertisement

dac03 shatter

29 %
71 %
advertisement
Information about dac03 shatter
Education

Published on January 16, 2008

Author: Regina1

Source: authorstream.com

advertisement

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!

Add a comment

Related presentations

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 ...
Read more

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
Read more

dac03-shatter - Ace Recommendation Platform - 1

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

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 ...
Read more

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
Read more

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
Read more

symCon02-slides - Ace Recommendation Platform - 13

dac03-shatter; BET-issta04; isc07-almost; aspdac05-dynsym; issta04; MargotSlidessym_hand; Ramani-DATE04; Recommended Topics; np complete; decision problem ...
Read more

Google

Advertising Programmes Business Solutions +Google About Google Google.com © 2016 - Privacy - Terms. Search; Images; Maps; Play; YouTube; News; Gmail ...
Read more