dac03 shatter

Information about dac03 shatter

Published on January 16, 2008

Author: Regina1

Source: authorstream.com

Content

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!

Related presentations


Other presentations created by Regina1

Romantic Period Intro
15. 01. 2008
0 views

Romantic Period Intro

era7
17. 01. 2008
0 views

era7

English Technical Writing
19. 03. 2008
0 views

English Technical Writing

The Globalization of HIV
11. 01. 2008
0 views

The Globalization of HIV

Araki
08. 05. 2008
0 views

Araki

CLDP Presentation AU 2006
07. 05. 2008
0 views

CLDP Presentation AU 2006

P2 4 Liu Yu RFIDlab in CAISA
02. 05. 2008
0 views

P2 4 Liu Yu RFIDlab in CAISA

Lesson38 The Olympic Games
02. 05. 2008
0 views

Lesson38 The Olympic Games

2010Bid Park
30. 04. 2008
0 views

2010Bid Park

roysembel smak7
24. 04. 2008
0 views

roysembel smak7

jbartram
22. 04. 2008
0 views

jbartram

KJ1E0019
21. 04. 2008
0 views

KJ1E0019

Guides Saga
18. 04. 2008
0 views

Guides Saga

investing in costarica
17. 04. 2008
0 views

investing in costarica

Barg PAC3
10. 01. 2008
0 views

Barg PAC3

cisco systems dwdm primer oct03
11. 01. 2008
0 views

cisco systems dwdm primer oct03

Mark Regier
13. 01. 2008
0 views

Mark Regier

Coherence 1
15. 01. 2008
0 views

Coherence 1

WonnacottPhase1
16. 01. 2008
0 views

WonnacottPhase1

Micro Clim
17. 01. 2008
0 views

Micro Clim

geoterm
22. 01. 2008
0 views

geoterm

handout 186663
23. 01. 2008
0 views

handout 186663

similars
23. 01. 2008
0 views

similars

Customer Presentation
04. 02. 2008
0 views

Customer Presentation

part3 storms
11. 02. 2008
0 views

part3 storms

Gherm
12. 02. 2008
0 views

Gherm

Strawberries and Blueberries
22. 01. 2008
0 views

Strawberries and Blueberries

2007921162811471
28. 01. 2008
0 views

2007921162811471

treasuresbg
29. 01. 2008
0 views

treasuresbg

display advertising
29. 01. 2008
0 views

display advertising

telecom
31. 01. 2008
0 views

telecom

zhizhan
06. 02. 2008
0 views

zhizhan

TT IntroAfrica VCT
10. 01. 2008
0 views

TT IntroAfrica VCT

Parsons bores
13. 02. 2008
0 views

Parsons bores

Traditional music of Japan
13. 02. 2008
0 views

Traditional music of Japan

Ch14slideswebsitefin al7222006
18. 02. 2008
0 views

Ch14slideswebsitefin al7222006

classrocks
10. 01. 2008
0 views

classrocks

Microsoft Longhorn
20. 02. 2008
0 views

Microsoft Longhorn

ISV App Hosting for SaaS
21. 02. 2008
0 views

ISV App Hosting for SaaS

Iain Macleod Stephen Potts
29. 02. 2008
0 views

Iain Macleod Stephen Potts

poetry2007
11. 03. 2008
0 views

poetry2007

Crim Proc Sat Class 6
28. 01. 2008
0 views

Crim Proc Sat Class 6

Geology of Terrestial Planets
15. 03. 2008
0 views

Geology of Terrestial Planets

Minjun PhD Oral Exam
16. 03. 2008
0 views

Minjun PhD Oral Exam

Ontology of TB 16 9 04
20. 03. 2008
0 views

Ontology of TB 16 9 04

20070315presentation
24. 03. 2008
0 views

20070315presentation

harder2006wasteelvs
12. 02. 2008
0 views

harder2006wasteelvs

IPE Mutlinationals2005
31. 03. 2008
0 views

IPE Mutlinationals2005

39179261
08. 04. 2008
0 views

39179261

astrobiology
24. 01. 2008
0 views

astrobiology

The Panel of Chefs Of Ireland
05. 02. 2008
0 views

The Panel of Chefs Of Ireland

AMEDOC 2004 EXP RESP
15. 01. 2008
0 views

AMEDOC 2004 EXP RESP

otqh
10. 03. 2008
0 views

otqh

A C 4 US CHAPTER
13. 01. 2008
0 views

A C 4 US CHAPTER

chap5a
28. 02. 2008
0 views

chap5a

nih coprrace and trust
11. 01. 2008
0 views

nih coprrace and trust

ppt 44
14. 02. 2008
0 views

ppt 44

Morley TheLongandWindingRoa d1
04. 02. 2008
0 views

Morley TheLongandWindingRoa d1

abacus
11. 02. 2008
0 views

abacus

aaai99
25. 01. 2008
0 views

aaai99

DeCourcey Benefits 25Aug05
22. 01. 2008
0 views

DeCourcey Benefits 25Aug05

Holt
05. 02. 2008
0 views

Holt

Cmtg Dec11
09. 01. 2008
0 views

Cmtg Dec11

Modified Micro May 2003
08. 01. 2008
0 views

Modified Micro May 2003

egs poster
22. 01. 2008
0 views

egs poster