Fast SAT through Incremental Unit PropagationOutlineReconfiguring for a Failed EngineDiagnosis and Reconfiguration Performance on CassiniSlide 5Unit Propagation ExamplesSlide 7Unit PropagationSlide 9Slide 10Slide 11Slide 12DPLL ExampleDPLL Procedure [Davis, Putnam Logmann, Loveland, 1962]Slide 15Satisfiability with Incremental Unit Propagation (aka Truth Maintenance)Propagating Incrementally: Adding Clause C1Undoing Propagation Incrementally: Deleting Clause DSlide 19Slide 20Slide 21Slide 22Slide 23Slide 24Cassini PerformanceUnit Propagation in Real-Time: LTMSSlide 27Example: DS-1 Bus CommunicationLTMS’ Conservative Re-Support StrategySlide 30Slide 31Slide 32Slide 33Slide 34Slide 35Slide 36Slide 37Slide 38Slide 39ITMS: Re-Support via Local Cycle DetectionSlide 41Add Before DeleteAdd Before Delete -> Propagation blockedIdea: Roll back Consequences of C10 Just Enough to Let C11 ThroughSlide 46Slide 47ITMS: Roll Back by Repairing ConflictsSlide 51Slide 52Slide 53Slide 54Slide 55ITMS significantly decreases extra label changesComparing the ITMS to the LTMS9/20/2000 copyright Brian Williams 1Fast SAT through Incremental Unit PropagationTruth Maintenance and the ITMSBrian C. Williams Oct. 30th, 2002 16.412J/6.834J9/20/2000 copyright Brian Williams 2Outline•Motivation: Fast Mode Estimation and Reconfiguration•Review of unit propagation•Incremental unit propagation astruth maintenance9/20/2000 copyright Brian Williams 3Reconfiguring for a Failed EngineFire backupengineValve failsstuck closedOpen fourvalvesFuel tankFuel tankOxidizer tankOxidizer tank4copyright Brian Williams9/20/2000Diagnosis and Reconfiguration Performance on CassiniFailurescenarioMI time(Sparc 5 in sec)MR time(Sparc 5 in sec)MI time(est Sparc 5 sec)MR time(est Sparc 5 sec)EGApreaim2.2 1.7 .07 .17BPLVD2.7 2.9 .18 .29IRU1.5 1.6 .02 .03EGA burn2.2 3.6 .08 .03ACC2.5 1.9 .04 .02ME toohot2.4 3.8 .18 .78Acc low5.5 6.1 .25 .05Number of components: 80Number of clauses: 11,1019/20/2000 copyright Brian Williams 5Outline•Motivation: Fast Mode Estimation and Reconfiguration•Review of unit propagation•Incremental unit propagation astruth maintenance9/20/2000 copyright Brian Williams 6Unit Propagation Examples•C1: Not A or B•C2: Not C or A•C3: Not B or C•C4: AC1 C3C4ATrueBTrueCTrue9/20/2000 copyright Brian Williams 7Unit Propagation Examples•C1: Not A or B•C2: Not C or A•C3: Not B or C•C4: A•C4’: Not BC1 C3C4C1C2C4’ATrueBTrueCTrueAFalseBFalseCFalse9/20/2000 copyright Brian Williams 8C1 : ¬r q pr qpC2: ¬ p ¬ ttrue falsetprocedure propagate(C) // C is a clauseif all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l andfor each clause C’ mentioning “not l”, propagate(C’)end propagateUnit Propagation9/20/2000 copyright Brian Williams 9C1 : ¬r q pr qpC2: ¬ p ¬ ttrue falsetruetprocedure propagate(C) // C is a clauseif all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l andfor each clause C’ mentioning “not l”, propagate(C’)end propagateUnit Propagation9/20/2000 copyright Brian Williams 10C1 : ¬r q pr qpC2: ¬ p ¬ ttrue falsetruetprocedure propagate(C) // C is a clauseif all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l andfor each clause C’ mentioning “not l”, propagate(C’)end propagateUnit Propagation9/20/2000 copyright Brian Williams 11r qptrue falsetrueprocedure propagate(C) // C is a clauseif all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l andfor each clause C’ mentioning “not l”, propagate(C’)end propagateC2: ¬ p ¬ ttC1 : ¬r q pUnit Propagation9/20/2000 copyright Brian Williams 12r qpC2: ¬ p ¬ ttrue falsetruetfalseprocedure propagate(C) // C is a clauseif all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l andfor each clause C’ mentioning “not l”, propagate(C’)end propagateC1 : ¬r q pUnit Propagation9/20/2000 copyright Brian Williams 13DPLL ExampleExample:•C1: Not A or B•C2: Not C or A•C3: Not B or CAF TPropagate:C = FB = FA = FPropagate:B = TC = TA = T9/20/2000 copyright Brian Williams 14DPLL Procedure[Davis, Putnam Logmann, Loveland, 1962]DPLL(phi,A) Input: A cnf theory phi, an assignment A to propositions in phiOutput: A decision of whether phi is satisfiable.1. propagate(phi);2. If a clause is violated return(false);3. Else if all propositions are assigned return(true);4. Else Q = some unassigned proposition in phi;6. Return (DPLL(phi, A[Q = True]) or 7. DPLL(phi, A[Q = False])9/20/2000 copyright Brian Williams 15Outline•Motivation: Fast Mode Estimation and Reconfiguration•Review of unit propagation•Incremental unit propagation astruth maintenance•LTMS•ITMS9/20/2000 copyright Brian Williams 16Satisfiability with Incremental Unit Propagation (aka Truth Maintenance)•When adding an assignment incrementally introduce additional unit propagations (already done for DPLL)•When removing an assignment (backtracking), only remove propagations of that assignment.9/20/2000 copyright Brian Williams 17r qpC2: ¬ p ¬ ttrue falsetruetfalseprocedure propagate(C) // C is a clauseif all literals in C are false except l, and l is unassigned then assign true to l and record C as a support for l andfor each clause C’ mentioning “not l”, propagate(C’)end propagateC1 : ¬r q pPropagating Incrementally: Adding Clause C19/20/2000 copyright Brian Williams 18procedure unsupport(D) // D is a clauseif D supports some proposition pthen delete p’s support and truth assignment; for each support C containing p // Delete consequencesunsupport(C); for each clause A containing p // Resupport p then propagate(A);end unsupportUndoing Propagation Incrementally: Deleting Clause DsD: ¬r q pr qpC: ¬ p ¬ tA: ¬ s ¬ ptrue9/20/2000 copyright Brian Williams 19procedure unsupport(D) // D is a clauseif D supports some proposition pthen delete p’s support and truth assignment; for each support C containing p // Delete consequencesunsupport(C); for each clause A containing p // Resupport p then propagate(A);end unsupportsD: ¬r q pr qpC: ¬ p ¬ tA: ¬ s ¬
View Full Document
Unlocking...