On Finding All Minimally Unsatisfiable Subformulas

On Finding All Minimally Unsatisfiable Subformulas

On Finding All Minimally Unsatisfiable Subformulas Mark Liffiton and Karem Sakallah University of Michigan {liffiton, karem}@eecs.umich.edu June 21, 2005 Problem Description Given: Infeasible set of constraints C Goal: All Minimal Unsatisfiable Subsets of C AKA MUSes Minimal Unsat.: All proper subsets satisfiable

Compact explanations of infeasibility {C1,C2,C3,C4,C5} UNSAT {C1,C3,C4} UNSAT (MUS) { C3,C4} SAT {C1, C4} SAT {C1,C3 } SAT 2 Running Example Boolean CNF example: = = (a) (a) ((a) a) ((aa b) b) ((b) b) 4 constraints (clauses)

2 MUSes: MUS1 = {(a),(a)} MUS2 = {(a),(a b),(b)} 3 Outline Problem Description Motivation Maximal Satisfiability / Minimal Unsatisfiability Algorithms

Experimental Results Future Work 4 Motivation Diagnosis of infeasibility User feedback User creates constraint system. Infeasible when expect/require feasibility. MUSes point user to minimized causes of infeasibility. Aid understanding of large, infeasible systems Automatic processes Generally: Any process that needs to reason about infeasible constraint systems

Counterexample-guided abstraction refinement (CEGAR) in model checking systems 5 Why All MUSes? Generally: A set of constraints is infeasible as long as it contains any MUSes Correcting one MUS may leave others Optimal corrections could require knowledge of all MUSes Specific example: CEGAR

Abstraction used to reduce state space MUSes used to generalize spurious counterexamples for refinement of abstraction Many generalizations possible, many of them induce poor refinement 6 First Step: Max-SAT and MSSes Max-SAT Maximum cardinality satisfiable set of clauses Maximal Satisfiable Subsets (MSSes) Inaugmentable satisfiable set of clauses

(a) (a) (a b) (b) = =(a) (a)((a) a)((aab) b)((b) b)

7 A Hint of Duality MSS Satisfiable Cannot be made larger MUS Unsatisfiable Cannot be made smaller 8

Another Step: CoMSSes A CoMSS is the complement of an MSS (a) (a) (a b) (b)

==element element of ofMSS MSS ==element element of ofCoMSS CoMSS Each CoMSS provides an irreducible fix to the formula: removing its clauses makes the formula satisfiable (turns it into an MSS). = =(a) (a)((a) a)((aab) b)((b) b)

9 The Link: CoMSSes and MUSes Known: 1. A formula is SAT iff it contains no MUSes 2. Removing the clauses in a CoMSS from a formula makes it SAT Removing the clauses in a CoMSS removes at least one clause from every MUS in a formula. Every CoMSS is an irreducible hitting set of the collection of all MUSes. 10 Hitting Sets in the Example

Given a collection of sets M, a hitting set of M is a set that contains at least one element from each set in M. MUS1 = {(a),(a)} MUS2 = {(a),(a b),(b)} CoMSS1 = {(a)} CoMSS2 = {(a),(a b)} CoMSS3 = {(a),(b)} = =(a) (a)((a) a)((aab) b)((b) b) 11 The Duality: CoMSSes and MUSes Additionally, each MUS is an irreducible hitting set of the collection of all CoMSSes

Hitting sets provide a transformation from one collection to the other hitting sets CoMSSes MUSes hitting sets 12 Exploiting the Relationship In practice, finding satisfiable subsets of constraints is easier than unsatisfiable i.e., MSSes easier to find than MUSes

Because SAT is easier than UNSAT How to Find All MUSes: Find CoMSSes Compute minimal hitting sets of the CoMSSes 13 Outline Problem Description Motivation Maximal Satisfiability / Minimal Unsatisfiability

Algorithms Experimental Results Conclusions and Future Work 14 Algorithms for Finding All MUSes Separate steps CAMUS (Compute All Minimal Unsatisfiable Subsets Liffiton & Sakallah) Interleaved steps DAA (Dualize and Advance Bailey & Stuckey)

15 CAMUS: Finding All CoMSSes Augment CNF with clause selector variables Ci = xi1 xi2 xin becomes Ci = yi xi1 xi2 xin Y-variables permit enabling/disabling constraints within DPLL-style search A CoMSS can be obtained by solving an optimization problem Find a solution to the augmented formula with the fewest y-variables assigned FALSE

Add blocking clauses to block old solutions 16 CAMUS: Finding All CoMSSes Optimization: Solve incrementally using a sliding objective Start by finding all CoMSSes w/ 1 clause, then all w/ 2, etc until all found Implemented with an AtMost constraint Within a single bound, the algorithm can utilize a single incremental search, exploiting all common SAT techniques (esp. learned clauses) 17 CAMUS: Finding All

CoMSSes = =(a) (a)((a) a)((aab) b)((b) b) Clauses y1 a a y2 a a y3ba b a b y4 b y1 y2 y3 1. Add clause-selector variables 2. Add AtMost constraint 3. First solution y1 is FALSE Add blocking clause and COMSS 4. No further solutions, increment AtMost 5. Second solution y2 and y3 are FALSE Add blocking clause and CoMSS

CoMSSes {a} {a, a b} {a, b} 6. Third solution y2 and y4 are FALSE Add blocking clause and CoMSS 7. No further solutions, even without AtMost constraint y2 y4 AtMost({y1 ,y2,y3,y4} , 2) 1) 18 CAMUS: Obtaining a Single MUS Goal: Irreducible Hitting Set Straightforward construction, no search

Iteratively choose clauses to add to MUS Choice can be arbitrary For each chosen clause, alter remaining problem to make that clause essential 19 CAMUS: Obtaining a Single MUS CoMSS1 = {(a)} CoMSS2 = {(a),(a b)} CoMSS3 = {(a),(b)} 1. Select a clause to add to the MUS (a b) = =(a) (a)((a) a)((aab) b)((b) b)

20 CAMUS: Obtaining a Single MUS CoMSS1 = {(a)} CoMSS2 = {(a),(a b)} CoMSS3 = {(a),(b)} 1. Select a clause to add to the MUS (a b) 2. Select a CoMSS in which it appears (CoMSS2) = =(a) (a)((a) a)((aab) b)((b) b) 21 CAMUS: Obtaining a Single

MUS CoMSS1 = {(a)} CoMSS2 = {(a),(a b)} CoMSS3 = {(a),(b)} 1. Select a clause to add to the MUS (a b) 2. Select a CoMSS in which it appears (CoMSS2) 3. Remove any other clauses in that CoMSS from the problem This makes the chosen clause essential for that CoMSS = =(a) (a)((a) a)((aab) b)((b) b) 22

CAMUS: Obtaining a Single MUS CoMSS1 = {(a)} CoMSS2 = {(a b)} CoMSS3 = {(b)} 1. Select a clause to add to the MUS (a b) 2. Select a CoMSS in which it appears (CoMSS2) 3. Remove any other clauses in that CoMSS from the problem This makes the chosen clause essential for that CoMSS 4. Remove any CoMSSes in which the clause appears They are now hit by the MUS = =(a) (a)((a)

a)((aab) b)((b) b) 23 CAMUS: Obtaining a Single MUS CoMSS1 = {(a)} CoMSS3 = {(b)} 1. Select a clause to add to the MUS (a b) 2. Select a CoMSS in which it appears (CoMSS2) 3. Remove any other clauses in that CoMSS from the problem This makes the chosen clause essential for that CoMSS 4. Remove any CoMSSes in which the clause appears

They are now hit by the MUS 5. Iterate until no CoMSSes remain = =(a) (a)((a) a)((aab) b)((b) b) 24 CAMUS: Obtaining All MUSes Use general form of single MUS method Branch on choice of clause and CoMSS to make all possible MUSes

Tree is not irredundant, so ordering heuristics and memoization are used to prune / limit the tree size Very fast in practice: Millions of MUSes in minutes 25 Bailey & Stuckeys Algorithm Dualize And Advance (DAA) Finds CoMSSes by growing MSSes Interleaves MUS construction w/ MSS search 26

DAA: Finding CoMSSes Grow MSS from a satisfiable seed Add corresponding CoMSS to collection = =(a) (a)((a) a)((aab) b)((b) b) a a MSS={a , ab} a b b 27 DAA: Computing Hitting Sets

Calculate irreducible hitting sets of CoMSSes after each additional CoMSS is found Incremental cross-product Minimize results HS1={a} HS2={ab , b} New Hitting Sets New CoMSS {a} {a , a} {ab , b , a} Minimize (remove subsumed)

= =(a) (a)((a) a)((aab) b)((b) b) 28 DAA: Computing Hitting Sets Check each new hitting set for satisfiability If UNSAT, add to collection of MUSes If SAT, use as seed for growing next MSS New Hitting Sets {a , a} {ab , b , a}

Both are UNSAT, both are MUSes None are SAT, thus done 29 Comparison for Boolean CNF Overall: CAMUS is much faster than DAA for Boolean CNF (Usually about 2-3 orders of magnitude faster) Mostly due to: Integration with SAT solver Calculating hitting sets once, not checking them for SAT/UNSAT 30

Experimental Results 1000 Runtime to find all MUSes (in seconds) for 32 benchmarks, sorted by increasing CAMUS runtime DAA CAMUS >600 100 10 1 0.1 0.01 31 Future Work

Relaxations / approximations Trade off completeness/correctness for speed Find fewer than all MUSes Find non-minimal USes Utilize ideas from Dualize and Advance Investigating further applications of the algorithm Anywhere that constraints are used, potentially

New territory, due to novelty of solution 32 Thank You 33 Related Work Finding a single US (potentially multiple) Bruni & Sassano, zCore, AMUSE, others Boolean CNF Modify or use information from a standard SAT search Chinneck, et al Linear programs Irreducible Infeasible Subset (IIS)

None guarantee minimality (irreducibility) Minimizing a US to an MUS Jinbo Huang: A Minimal Unsatisfiability Prover 34 Related Work (cont.) Theoretical work Complexity of identifying MUSes Deciding whether a CNF formula is minimally unsatisfiable is DP-Complete Complexity bounds on identifying certain classes of MUSes

35

Recently Viewed Presentations

  • Summer Surf - holcombegrammar.org.uk

    Summer Surf - holcombegrammar.org.uk

    A quick warning that UCAS do make slight changes to their web-site appearance on a yearly basis so although many of the tabs you are asked to go to will still be there, they may not always be where I...
  • Meglan Vlach - University of Michigan

    Meglan Vlach - University of Michigan

    Meglan Vlach Terrence Szymanski Ling 512 Fall 2005
  • GCSE Languages - Whitchurch High School

    GCSE Languages - Whitchurch High School

    The new GCSE: Study skills required: Identify general information. Identify an overall message. Find key points / specific details. Opinions. Deducing meaning. Recognising and responding to key information (themes and ideas) Scanning - organising and presenting information. Drawing inferences /...
  • Sample HR PowerPoint Template

    Sample HR PowerPoint Template

    The Performance and Staff Development Program Making the Process Work for You Performance and Staff Development Program Goals Provide accurate, written feedback on performance and accomplishments for the appraisal cycle Establish performance goals/expectations for coming cycle Address professional development needs...
  • Peer Services & Supports: Models & Research Evidence

    Peer Services & Supports: Models & Research Evidence

    Peer-Delivered Health Promotion Models & Research Evidence. Judith A. Cook, Ph.D. Professor and Director. Center on Mental Health Services Research & Policy. Department of Psychiatry. University of Illinois at Chicago. Presented at Fogarty UIC Global Mental Health & Migration Research...
  • Hospitality & Tourism Overview Charlotte City Council May

    Hospitality & Tourism Overview Charlotte City Council May

    More than 124,000 jobs in the hospitality and leisure sector, with direct visitor spending supporting 63,000 of those jobs. One in nine people in Charlotte work in the hospitality and leisure sector . Source: CRVA. Tourism Tax Overview.
  • Introduction to the Finite Element Method

    Introduction to the Finite Element Method

    Times New Roman Default Design The Finite Element Method Course Outline Course Outline con't Course outline con't Course outline con't Course outline con't Course outline con't Course outline con't Course outline con't
  • Belt Sander Safety - Helena Middle School

    Belt Sander Safety - Helena Middle School

    Tahoma Arial Wingdings Calibri Slit 1_Slit Belt/Disc Sander Safety Belt Sander Safety Belt Sanders ...