# SymChaffAAAI05

43 %
57 %
Education

Published on February 26, 2008

Author: worm

Source: authorstream.com

SymChaff: A Structure-Aware Satisfiability Solver:  SymChaff: A Structure-Aware Satisfiability Solver Ashish Sabharwal University of Washington, Seattle AAAI, July 2005 SAT: The Satisfiability Problem:  SAT: The Satisfiability Problem Input: Boolean formula F in CNF F = (x1 OR x2) AND (x1 OR x3 OR x4) AND … Output: “satisfying assignment” or “unsat” NP-complete, hence difficult but useful! Problem instance e.g. planning, verification, design, … CNF Encoder F domain dependent sat unsat SAT Solver general purpose SAT: The Satisfiability Problem:  SAT: The Satisfiability Problem Numerous real-world applications hardware verification, testing, planning, scheduling, design automation, … Dozens of academic/industrial SAT solvers e.g. Grasp [MarquesSilva-Sakallah-96], Relsat [Bayardo-Schrag-97], SATO [Zhang-97], zChaff [Moskewicz-etal-01], Berkmin [Goldberg-Novikov-02], March-eq [Huele-vanMaaren] Most don’t exploit problem structure well! Planning Example: Logistics:  Planning Example: Logistics Each city has several boxes Each box has a destination city Several trucks at a base station CityA CityB CityD CityC Task: use trucks to move boxes to their resp. destinations Domain knowledge: All trucks are equal! SAT and Symmetry:  SAT and Symmetry Natural symmetry in many domains, e.g. planning: all trucks at a base station, all nails in assembly circuit design: all wires connecting two switch boxes multi-processor scheduling: all processors cache coherency protocols: all caches “If k trucks need to be sent from CityA to CityB, w.l.o.g. send the first k.” Proposed techniques have several drawbacks Easy for humans, hard for SAT solvers! Our Solution: SymChaff:  Our Solution: SymChaff Captures a wide class of natural symmetries by incorporating variable semantics Exploits high level problem structure rather than “flat” CNF formulation F sat unsat Problem instance CNF Encoder SAT Solver Previous Approaches – 1/4:  Previous Approaches – 1/4 Symmetry Breaking Predicates [Crawford-etal-96] e.g. Shatter [Aloul-Markov-Sakallah-03] F sat unsat SAT Solver SBP generator SBP SBPs can be prohibitively many, too large, difficult to compute (graph isomorphism) F’ Previous Approaches – 2/4:  Previous Approaches – 2/4 pseudoBoolean tools: counting constraints e.g. PBS [Aloul-Ramani-Markov-Sakallah-02], pbChaff [Dixon-Ginsberg-Parkes-04], Galena [Chai-Kuehlmann-03] Problem instance pbCNF Encoder pbCNF sat unsat pbSAT Solver some domains provably hard (e.g. clique color) implicit counting representation not always suitable Previous Approaches – 3/4:  Previous Approaches – 3/4 Handle symmetries dynamically in search e.g. sEqSatz [Li-Jurkowiak-Purdom-02], another solver [Dixon-Ginsberg-Luks-Parkes-04] F sat unsat SYM-SAT Solver expensive group-theoretic computations Previous Approaches – 4/4:  Previous Approaches – 4/4 Domain specific solutions Testing [MarquesSilva-Sakallah-97], model checking [Shtrichman-04], planning [Rintanen-03, Fox-Long-99] Domain specific Cannot exploit advances in SAT solvers [Fox-Long-99] Very similar to our technique; yields non-optimal parallel plans Our Contribution:  Our Contribution New framework for symmetry in SAT Low overhead, top-down approach Seamless integration with current SAT solvers Foundation in many-sorted First Order logic SAT solver SymChaff that extends zChaff Outperforms previous approaches on several domains from theory, planning, and design Philosophical: a tiny bit of non-CNF input can dramatically speed up SAT solvers Key Ideas:  Key Ideas Symmetry Representation Multi-way Branching Symmetric Learning Planning Example: Logistics:  Planning Example: Logistics Task: use n trucks to move boxes to their resp. destinations Problem variables: mv_tr3_cD_time1 load_boxA1_tr1_time1 … Possible solution: begin by sending some trucks to cityA CityA CityB CityD CityC Idea #1: Multi-way Branching:  Idea #1: Multi-way Branching Typical SAT solver: - effectively explore 2n branches for mv_tr?_cA mv_tr1_cA 0 1 mv_tr2_cA 1 0 Idea #1: Multi-way Branching:  Idea #1: Multi-way Branching Idea is extended to “multi-class symmetry” e.g. let boxA1, boxA2 be symmetric as well variable load_boxA1_tr1 symmetric to variable load_boxA?_tr? Issues: How is symmetry information provided? How is it maintained as we branch? Idea #2: Symmetry Representation:  Idea #2: Symmetry Representation Input to SymChaff includes: Symmetry classes for objects e.g. tr1, …, trn belong to class TR Semantics for variables e.g. mv_tr1_cA is indexed by class TR Symmetry sets of objects; dynamic initially: {tr1, …, trn} is a symmetry set branch and send tr1, tr2 to cityA: split/refine set into {tr1, tr2}, {tr3, …, trn} backtrack: re-unite these two sets Idea #3: Symmetric Learning:  Idea #3: Symmetric Learning A “sym-conflict clause” is learnt NOTE: this replaces the triedGroups approach of [Fox-Long-99]; doesn’t suffer from non-optimality of parallel plans … send j trucks to cityA Fail: too few trucks left for other cities! SymChaff learns that these branches need not be explored Fail Experimental Results:  Experimental Results Compared SymChaff with zChaff (winner of SAT’04 competition; industrial category) March-eq-100 (winner of SAT’04 competition; hand-made category) zChaff + Shatter (using SBP) Galena and pbChaff (pseudoBoolean solvers) (on some domains; see paper) Problem domains Theory: pigeonhole, clique coloring Planning: gripper, logistics (2) Circuit design: channel routing Representative Runtime Samples:  Representative Runtime Samples * denotes > 6 hours Best SAT solvers don’t do very well! Computing SBPs may be expensive! Computing SBPs may not help! Problem may be really hard! And all this from…:  And all this from… Original STRIPS specification: (objects tr1 tr2 tr3 boxA1 boxA2 boxB1 boxB2 ...) (actions ...) (init ...) ... New STRIPS specification: (objects tr1 tr2 tr3 – symTrucks boxA1 boxA2 – symBoxA boxB1 boxB1 – symBoxB ...) (actions ...) (init ...) ... Conclusion:  Conclusion New framework that efficiently incorporates symmetry into SAT solvers Domain independent Low overhead Exploits high level problem description Can this framework help local search? Can we extend it to handle new symmetries that arise during the search? E.g. AirLock domain [Fox-Long-02] Ongoing and Future Work:  Ongoing and Future Work Use symmetry framework elsewhere local search techniques like Walksat improved variable selection heuristic Handle new symmetries as they arise e.g. AirLock domain of [Fox-Long-02] Easy extensions implement in pseudoBoolean solver create PDDL-to-SYM converter for planning Improvements to SymChaff other symmetric learning schemes dynamic selection in multi-way branches

 User name: Comment:

## Related pages

### SymChaff: A Structure-Aware Satisfiability Solver

SymChaff: A Structure-Aware Satisﬁability Solver Ashish Sabharwal Computer Science and Engineering University of Washington, Box 352350 Seattle, WA 98195 ...

### AAAI05: SymChaff: A Structure-Aware Satisfiability Solver

SymChaff: A Structure-Aware Satisfiability Solver Ashish Sabharwal University of Washington, Seattle AAAI, July 2005

### AAAI05-SymChaff-A-StructureAware-Satisfiability-Solver ...

View and Download PowerPoint Presentations on AAAI05 SYMCHAFF A STRUCTUREAWARE SATISFIABILITY SOLVER PPT. Find PowerPoint Presentations and Slides using ...