logging in or signing up dac03 shatter Regina1 Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINTLite Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 64 Category: Education License: All Rights Reserved Like it (0) Dislike it (0) Added: January 16, 2008 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript 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 MichiganMotivation …: 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 symmetriesSymmetries 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 SymmetriesSymmetry 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 ConclusionsPermutations 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 spaceFull 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 literalsLinear-Sized PPs: Linear-Sized PPs PP() size:4n clauses14n literals PP() size:5n clauses0.5n2 + 13.5n literalsLinear-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=1Partial 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 compositionsExperimental Results: Experimental Results % ofbits thatmap tothemselves Generators consisted of cycles of size 2 onlyExperimental Results*: Experimental Results* * Break generators onlyExperimental Results: Experimental Results Total size of generator-only SBPs using various SBP constructionsExperimental 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 constructionConclusions: 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! You do not have the permission to view this presentation. In order to view it, please contact the author of the presentation.
dac03 shatter Regina1 Download Post to : URL : Related Presentations : Share Add to Flag Embed Email Send to Blogs and Networks Add to Channel Uploaded from authorPOINTLite Insert YouTube videos in PowerPont slides with aS Desktop Copy embed code: (To copy code, click on the text box) Embed: URL: Thumbnail: WordPress Embed Customize Embed The presentation is successfully added In Your Favorites. Views: 64 Category: Education License: All Rights Reserved Like it (0) Dislike it (0) Added: January 16, 2008 This Presentation is Public Favorites: 0 Presentation Description No description available. Comments Posting comment... Premium member Presentation Transcript 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 MichiganMotivation …: 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 symmetriesSymmetries 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 SymmetriesSymmetry 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 ConclusionsPermutations 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 spaceFull 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 literalsLinear-Sized PPs: Linear-Sized PPs PP() size:4n clauses14n literals PP() size:5n clauses0.5n2 + 13.5n literalsLinear-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=1Partial 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 compositionsExperimental Results: Experimental Results % ofbits thatmap tothemselves Generators consisted of cycles of size 2 onlyExperimental Results*: Experimental Results* * Break generators onlyExperimental Results: Experimental Results Total size of generator-only SBPs using various SBP constructionsExperimental 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 constructionConclusions: 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!