ࡱ> MOUVN@=0(ρ_42w\!-fEx՚?lEߞc;X!Ba;߿4D&9R(P$c`)8&gȠDqG YH  $ .(}3Ƴ3w k=~ͼ]'D2魗ѯ f>.M<}.ͷ.܄λm:+n$|lbLoK#;slgwviJK4GG?W HẖvqWTv^RJJ1:7ZÞnIk#zy=6[h~ L lis\ /͹C!i!?JұE;a_E>l>MzEs&}/}Ή-h *a\0ϣssyAkF۹h60~zsŘ.pVj|d>w*=Db=VJ*O7̹M_byߊ'O!~2Aߞ(ؘl<͵h+d|훞~IN{;Sg+uO,bs]f-,Mi_b.U ?`Ӎ!ZMW4&=DYV+Q6-)5?Vbчl}Ki6_yD}*Wl[9tOmQ;n{D5~C;:5{bcq\1>)Ud!>1gOJ3m8CzgEeK\¼Œm=77=mhu+-vMjjlW-VsmzJjtMH?8y]g}#xWUNUIGzqT3!6~c[٪}|OCvcs^VH4'=|@̭nDty~CN摒=DSk}b|4=ESZe!n>#<@;h /J54TZ=ѪIu*Z4Fmu~lpY<̥kC{11;QQ4ׂ|뛏f _QUXpu4W+pm$;UCʅ[[&&m`mhڴ6W++׿hqvv'mp-^׷ÓWNĊ6Ϥy`E='䋗#'kxu!Oh9ل)'Nn@Mh-h=3NJ0V+.13n 3G3 |>1-Sb2g>uA'_bևO0Sbլ gP.ɱ&Ɩ/1Ĺ|3d riW> %f{\cM Qk]}f'%1kx.t\9 _b:oiۜIe2_T/J&g`nZ3/)۵pJT@1Zr %VkT2bȥ25rq/̗X\jCs1JG@xZkvYd @#- /ͧ eΤ׋F)Iֱ֡PΕӔf;ۥhA=iOZ*k1{wU|6% Sr59֚sevZ=3wf|;I;FT)?ҫVki+)֚|WZVYkU]iX+\^|WZq֊JK*Ԓ{t B~_C(S3?si@=A=9va+ Z[jWy4fxMhQEjTjXAxR`,"-)+"V[PAP4')`ozM- ֓xԙL6yLξg^~)v mV>k#CSZ~3hzѶ>a;Ԏ:dXm +'V <ctjA~m<̈^0;qy EBQ;9CGRFb4QM6>5%f(/_*U/FuοKlQ?w%_dƆ?d/ߴ?SS3%f_7{=Khr].0㉁/1U? 0@^0SbLs}^3nYӺ [/8s\ Yu !Ō?ĚW>+\X'jϸ|5[U\m٨>\)$5\51h]3- e~!B _bqoO*?AR{Ab %g.Y!e.Qk3^/VrgfQ,.<>m5iYd @#t\.gzѰOӐ}MΙF*POkN|R(z?hJAv&ZoqOZV:fuf.ڕϦwcvrZ J.VɡV系ۃ.&-9&je_ѯŭ5ZJkf5ߕ2k-k+5Z|WZ֪h+$שߕVҪҒ5,):'Q[;8j&ՠ 2%tgR9LF aK,n}=Wa2wxo s'&ӥo@3kNz2A'ȗXRг&ВXAu/$s\Np.{Adof|PaĒcΥ_z! _bI\Xr;u yD cA^O.zz\ 3%V=N,y1t&m2L2hĢǖw>_7nW_9gFwOj9EqeCi߾]KܓMXk%~ZMJ'-*0ZZK)j]bRZfw7g|OQ+zFS~k~ZZ5kii֪᧥Z놟VʆV'uOK+ZYUҒ5<*~ZrnAP_z01LF3'\Zx/@=`>h= \[jWy4xOHqo\fA{TKD(+IFDfBA' 7=t=钒hoB{og~[s;o~3QpZmU#FЃ=3 ~hgZʸ;m4Z8뜪bcc)>6O ۻj= `V.ɯ^4`qzv~m9nZOif]MKoF] hn"r J?15'4\!l;к: [f|%O3Y?Ⰽߥ4ㆅ/1~:?Ɍ7#r/3c_nOq 댟>O3&,|Ӑj62=Kyhyz_e _b-3T%dJ,ٛpORc}xmY/\=} \?SbYg>z^JZ,|ERˤg{LE3j;﯅<\k5\b9b%pBJ[oܞ -ךt|_.r.T0]\hQigK,:U:acs{]P1F1~%vsTsyd%K:dqD c~.z_ 2%:Gw2Gpۧhӏ6Ěbc1ۈE5Χ۪_rΤGkZ\cjZk&ZK'K%W´6ZǡV^VyǨ2L"kc4{TZ9.i #gqÏKk ?.UZ56Xk*VJXV2QU?.-gU?L-yF'S kw#mda?B@=yUp;&w!#қ\[jWy4nxMHTQyE H7*g$B "!WA;wp}&%\E` \=ǹλo|o|;ss4L"4z"mO@Y1_ytF%Qs}wz SieRcVEoKi_hml>֣5 /a `ݵ5$#GkHsi=DzJz -3U>1s6tR@j"5ZˆjxЎ7c遲8a0_sG+̿ 㾃8 ッ??!w/&wEq.cUXKa :/_/wnre` cV2$v29Z~\I-KZbu~ c\H-Ĭ%긌 c\ZcVL%ewLͥf e^~3v|%]~qo0\Ra\`לs>X0`4ًhj5˹jwz0c\c͸fj.yXuOs|ޖ5WM-n|`>oe_٧)!,c1}PXn 4LgLLj#5tO>wŇ{7hnYqEi۽];5Kcʤ)M؇W-6쥱s Zv^nH45"l?fģ].{tX1~i{ ׀Y+,^VkC6ؗWQV˫Eu5 b_^z Ob)NK54Jk=wOlFe.-~(   O|http://sat.inesc.pt/~jpms/research/tech-reports/RT-01-2002.pdf0bWorksheet Excel.Sheet.802Microsoft Excel Worksheet0bWorksheet Excel.Sheet.802Microsoft Excel Worksheet0bWorksheet Excel.Sheet.802Microsoft Excel Worksheet0bWorksheet Excel.Sheet.802Microsoft Excel Worksheetl03bWorksheet Excel.Sheet.802Microsoft Excel Worksheet04bWorksheet Excel.Sheet.802Microsoft Excel Worksheet 05bWorksheet Excel.Sheet.802Microsoft Excel Worksheetr06bWorksheet Excel.Sheet.802Microsoft Excel Worksheet0CbWorksheet Excel.Sheet.802Microsoft Excel Worksheet/0(  0;[0 0 000$([\{b00 000000000  0=] 0 0 0000 2 3 !A0C0E0G0I0c00000000000000000!%),.:;?]}acdeghijklmnop0DTimes New Roman@b@bLb0pbpb 0DArialNew Roman@b@bLb0pbpb 0" DWingdingsRoman@b@bLb0pbpb 00DSymbolgsRoman@b@bLb0pbpb 0@  @@``  @n?" dd@  @@`` @8 D@6  &&()2  FW\^x+}[ci%-ffXNLD`k oKY r3%{{~$NW* hX   0'"   :3'"   bqKKN qKWpC5 %  *    +/1.   !"#$ ,0-) 4'(7&4$"$0(ρ_42w"$Nؖ0Bͭ"$A=9va+ Z "$=e˒Vb `"$`>h= "$yUp;&w!#қ c $      A@  Ag  8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| 33AAAgggf@8  g4MdMd|b 0tb ppp? <4BdBdP@bL<4!d!dP@bLg4:d:d|b 0tb p@ pp?$ ICCAD'01O =6Hypothetical Reasoning in Propositional Satisfiability76RJoao Marques-Silva Technical University of Lisbon, IST/INESC, CEL Lisbon, PortugalRHypothetical ReasoningPreliminary ongoing research work Not yet published Main ideas available as a (preliminary) technical report: I. Lynce and J. Marques-Silva,  Hypothetical Reasoning in Propositional Satisfiability, Technical Report 1/2002, INESC-ID, March 2001 http://sat.inesc.pt/~jpms/research/tech-reports/RT-01-2002.pdf Some of the concepts still evolving Feedback welcome ! Joint work with Ines Lynce":%":%.n0n9U Motivation"SAT solvers have been the subject of significant improvements in recent years The utilization of SAT is increasing in industry More challenging problem instances Improvements to current key techniques unlikely(?) Better (non-chronological) backtracking? Better data structures? Newer (more competitive) strategies? How to improve SAT solvers? Devise new paradigms& Integrate already used techniques #3f9#3f!Outline/Notation & Definitions Evolution of SAT Solvers Overview established approaches Next challenges in SAT Other promising approaches Our proposed approach Hypothetical reasoning (HR) The overall approach Applying reasoning conditions Relation with other existing techniques Preliminary experimental results0 d3(!0 `3(!Notation & DefinitionsNCNF Formula, clauses, literals: A CNF formula (j) is a conjunction of clauses A clause (w) is a disjunction of literals A literal (l) is a propositional variable or its complement Assignments: x, 0 denotes the assignment of value 0 to variable x Can also use x = 0 to denote an assignment  b  !7 > (>Notation & Definitions (Cont d)Unit-clause rule: If clause w is unit (has a single free literal l), then the free literal l must be satisfied for the clause to be satisfied Iterated application of the unit-clause rule is referred to as unit propagation (UP) or boolean constraint propagation (BCP) BCP(x, vx): denotes the set of implied variable assignments obtained by applying BCP as the result of the triggering assignment x, vx If BCP( x, vx) unsatisfies one or more clauses, then we say that ^ BCP( x, vx) V $ { 5A Taxonomy of SAT Algorithms?+The Most Effective SAT SolversbBacktrack search Boolean constraint propagation  Reasonable branching heuristic Clause recording Non-chronological backtracking Search strategies Restarts Random backtracking Efficient data structures E.g. head/tail lists; watched literals; literal sifting Examples: BerkMin; Chaff; SATO; rel_sat; GRASPb8/b8/1Other Effective SAT SolversBacktrack search Unit propagation Chronological backtracking Fine-tuned branching heuristics Probing & reasoning techniques Lookahead (variable probing) Equivalency reasoning Search strategies Restarts Efficient data structures E.g. head/tail listsl|3 |3  Examples: EQSATZ Built on top of SATZ Uses equivalency reasoninig RAND-SATZ Built on top of SATZ Branching randomization Search restarts SATZ No search restarts No equivalency reasoning Forms of look-ahead probing~ 1 =H 1 =HOther Dedicated SAT SolversLocal search for dedicated classes of instances Incomplete class of algorithms Useful if instances known to be satisfiable Solvers with domain-specific information Incremental SAT SAT on Boolean networks & H0M),0M),Challenging Problem InstancesSAT is being applied in industrial settings Electronic design automation Formal verification of hardware/software systems & SAT solvers are expected to handle problem instances: that have hundred thousand / few million variables that have tens of million clauses that may be unsatisfiable SAT solvers must be capable of proving unsatisfiability completeness is a key issue ! ,Q7o8,Q7  #8 zChallenges to SAT Solvers Dramatic improvements to backtrack search SAT solvers unlikely Can utilize equivalency reasoning Hard to interact with clause recording and non-chronological backtracking Can apply lookahead techniques Hard to interact with clause recording and non-chronological backtracking Can devise new search strategies Search restarts, random backtracking, & ? ~?#JJ!+?#JJ!+`Other ApproachesResolution Unlikely to be a practical proof procedure Variable probing (branch-merge rule) Clause probing (recursive learning) Not (yet) extensively evaluated Additional mechanisms for identifying necessary assignments and inferring new clauses Integrated solution still lackingl ,I"V" ,I"V"Resolution (original DP)Iteratively apply resolution (consensus) to eliminate one variable each time i.e., resolution between all pairs of clauses containing x and x formula satisfiability is preserved Stop applying resolution when, Either empty clause is derived instance is unsatisfiable Or only clauses satisfied or with pure literals are obtained instance is satisfiableMf, 9  > R Y'  <Stalmarck s Method (SM) in CNF& oRecursive application of the branch-merge rule to each variable with the goal of identifying common conclusionsHp.!An Alternative Explanation for SMRecursive Learning (RL) in CNF&]Recursive evaluation of clause satisfiability requirements for identifying common assignments<^1!An Alternative Explanation for RL SM vs. RLBoth complete procedures for SAT Stalmarck s method (in CNF): hypothetical reasoning based on variables use variable assignment conditions to probe assignments variable probing Recursive learning (in CNF): hypothetical reasoning based on clauses use clause satisfiability conditions to probe assignments clause probing Both can be viewed as the process of identifying selective resolution operations Both can be integrated into backtrack search algorithms >ccR9>  : <R7,! The Objectives of HRIntegrate variable probing and clause probing Complete proof procedure for SAT Devise conditions for a priori identification of new clauses That entail most of existing clause inference procedures Evolve from identification of necessary assignments to generalized clause reasoning.!=9T !97  Applications: Complete proof procedure for SAT Preprocessing engine to existing SAT solvers With polynomial effort Replace unit propagation with HR with backtrack search solvers With polynomial effort Cooperate with backtrack search solvers In parallel solutions for SATN?)N?) The Organization of HR LRecursive procedure that: Extends variable probing To incorporate clause probing Ensures completeness Establishes general clause inference conditions That cover (most) existing clause inference conditions Readily implements a number of additional techniques 2-var equivalence; hyper resolution (with binary clauses); equivalency reasoning; binary clause inference conditions; & Can be integrated into backtrack search4175y( #75y(How to Implement HR ?Independent probing, given conditions on variables and on clauses, may not be practical O(L2+ L N) = O(L2) at each step L: number of literals N: number of variables Construct assignment & trigger tables, for implementing variable and clause probing O(L N) at each step In practice, worst-case complexity is extremely unlikely OBS: unrestricted clause inference conditions are computationally hard to implementX -T9TX - /9TAssignment Table rCaptures the result of applying BCP to each variable assignment Create a (2N x 2N) matrix: Each row is associated with an assignment x, vx 1-valued entries denote assignments y, vy implied by BCP due to trigger assignment x, vx, i.e. BCP(x, vx) OBS: In practice can use a sparse matrix representation ! [;[*+08 :Assignment Table (Example)b, 0 implies (with BCP) the assignments b, 0, c, 0 and d, 0 FFE Trigger Table BCaptures which variable assignments directly imply (w/ BCP) each variable assignment Create a (2N x 2N) matrix: Each row is associated with an assignment x, vx 1-valued entries denote assignments y, vy that imply, with BCP, the assignment x, vx OBS: The trigger table is the transpose of the assignment table ! Required to create trigger table if using a sparse matrix representation of the assignment tablepCap*+-@a Trigger Table (Example)b, 1 is implied (due to BCP) by the assignments a, 0, a, 1 and b, 1MML!Utilizations of Assignment Tables!Necessary assignments from variable assignment conditions  variable probing&M M!Utilizations of Assignment Tables!Necessary assignments from clause satisfiability conditions  clause probing Assuming existence of clause (b d) nM& t!Utilizations of Assignment Tables!4Clause inference from variable assignment conditions&5  5!Utilizations of Assignment Tables!6Clause inference from clause satisfiability conditions&7 6 Utilizations of Trigger Tables4Clause inference from variable assignment conditions&5 4Utilizations of Trigger Tables9Clause inference from clause unsatisfiability conditions &: 9!Reasoning Conditions Summary#Necessary assignments: From variable assignment conditions (variable probing) From clause satisfiability conditions (clause probing) Inferred clauses: Satisfiability conditions Variable assignments Clause satisfiability Unsatisfiability conditions Variable assignments Clause satisfiabilityn++%)++#Inference of ClauseszHR reasoning conditions can only infer binary clauses ? No. Can infer arbitrary clauses ! Clause satisfiability conditions: For each clause w = (t1 t2 tm) of formula j, all clauses of the form (s1 s2 sm), such that s1, s2,,sm BCP(t1, 1) & BCP(tm, 1), are implicates of j Clearly subsumption can potentially be applied Clause unsatisfiability conditions: For each set of assignments A = { t1, 0, t2, 0, , tm, 0 }, such that ^ BCP(t1, 0) BCP(t2, 0) BCP(tm, 0), then clause w = (t1 t2 tm) is an implicate of j 9#"0$6    0 !  >Reasoning Conditions Complexity'O(L N) for constructing assignment & trigger tables and implementing variable and clause probing Why ? BCP for filling each row is O(L) For the 2N rows, construction of table is O(L N) Each set intersection can trivially be accomplished in O(N) ! All intersections can be done in O((N + L) N) = O(L N) Corresponding to variable and clause probing Total time complexity is O(L N) OBS: In practice worst-case complexity extremely unlikely OBS: unrestricted clause inference conditions are computationally hard to implement; must use restrictionsthTw-!2"- ( The HR Algorithm Basic HR algorithm (with depth d, target variables V) return if depth d 0 For each variable v in set of target variables V For each assignment to variable v L1: Apply unit propagation (BCP) Apply (tabular) reasoning conditions Recur HR with depth (d-1) Re-apply (tabular) reasoning conditions [Optional] Loop from L1 if more assignments6G""h,61""h,TRelation with Other TechniquesTAssignment & Trigger tables naturally capture: Variable probing (branch-merge rule) Lookahead techniques Clause probing (recursive learning) New clause inference conditions Assignment & Trigger tables allow capturing: Failed-literal rule Two-variable equivalence Closure of binary clause implication graph Literal dropping Equivalency-reasoning / Inference of binary clauses Hyper resolution (with binary clause inference) & ?l/%D-/%D-Relation with Other TechniquesFailed literal rule: If an assignment x, 0 yields an unsatisfied clause, then x, 1 is a necessary assignment In the construction of the assignment table, If ^ BCP(x, 0), then x, 1 is a necessary assignment\-:K-   Relation with Other Techniques2-variable equivalence: First form: If both (x y) and (y x) exist in formula, then x y Second form: Utilize binary clause implication graph Identify strongly connected components (SCCs) If x, 0 and y, 0 in the same SCC, then x y If, from construction of the assignment table, y, 0 BCP(x, 0) and y, 1 BCP(x, 1), then x y Captures all SCCs in binary clause implication graph Can identify additional 2-variable equivalences !  < V3jh  V(/e  Relation with Other TechniquesClosure of binary clause implication graph: If l1, 1 l2, 1 and l2, 1 l3, 1, then l1, 1 l3, 1 and infer clause (l1 l3) From construction of the assignment table, if l2, 1 BCP(l1, 1), then create clause (l1 l2) Captures the identification of the transitive closure of the implication graph Can identify additional implications (and clauses) ! ,`e,     .wRelation with Other TechniquesLiteral dropping [Dubois & Dequen, IJCAI 01]: Given a clause w = (l1 l2 lk), if exists a proper subset of literals {s1, s2, & , sj } of w, such that ^ BCP(s1, 0 s2, 0 sj, 0), then create a new clause (s1 s2 sj), that subsumes w Using the assignment table, if exists a set of assignments A = { t1, 0, t2, 0, , tm, 0 }, such that ^ BCP(t1, 0) BCP(t2, 0) BCP(tm, 0), then create the clause: w = (t1 t2 tm) Two techniques similar, but not comparable Literal dropping less general (starts from existing clauses), but more accurate (considers BCP of set of assignments)T/ng+v-*    @ +v uRelation with Other TechniquesEquivalency reasoning [Li, AAAI 00]: Shown to be covered with: Unit propagation; 2-variable equivalence; conditions for inferring binary clauses Binary clause inference conditions [MS, CP 00]: Inference from pattern 2B/1T: Given (l1 x) (l2 x) (l1 l2 y), infer (x y) From the assignment table: If x, 0 y, 1, then infer the clause (x y)&R1;2$R/ * k Relation with Other Techniques8Binary clause inference conditions [MS, CP 00]: Inference from pattern 0B/4T: Given (l1 l2 x) (l1 l2 x) (l1 l2 y) (l1 l2 y), infer clause (x y) From the assignment table: Assume l1 = 0 (depth 1) Can infer (x y) (depth 2) From (l2 x) (l2 y), Assume l1 = 1 (depth 1) Can infer (x y) (depth 2) From ( l2 x) (l2 y), \ infer (x y) But HR with depth 2 required ! 1^ /      Relation with Other TechniquesHyper resolution (w/ binary clauses) [Bacchus, SAT 02]: Allows inference of binary clause Given (l1 x) (l2 x) (lk x) (l1 l2 lk y), infer (x y) From the assignment table: If x, 0 y, 1, then infer the clause (x y)9w27* * Preliminary ResultsImplemented reasoning conditions on top of JQuest Assigment tables Trigger tables Necessary assignments Probing due to variables and clauses (binary and ternary) Clause inference conditions Simplified version: only binary clauses can be inferred Results for reasoning conditions on example problem instances #Vars: number of variables; #Cls: number of clauses #NA: necessary of assignments; #IBC: inferred binary clauses26:8>q26:8>qExperimental ResultsImplementing/Completing HRImplement (efficient) recursive wrapper Incrementally define set of variables in recursive step Reduce significantly the number of row updates in assignment and trigger tables Instead of BCP-based reasoning conditions, evolve to clause-based reasoning conditions How to use HR? Standalone complete proof procedure ? Integrated within backtrack search SAT solver ? Hard to interact with clause recording and non-chronological backtracking Used as a preprocessing engine to backtrack search SAT solvers ?(8PWVJA(8PWVJA Conclusions Proposed the Hypothetical Reasoning algorithm Integrates variable probing (branch-merge rule) and clause probing (recursive learning) Implements a number of additional techniques That allow inferring new clauses That entail most existing clause inference conditions That entail a significant number of simplification techniques Preliminary results for practical problem instances: By applying reasoning conditions, a significant number of necessary assignments can be identified and a significant number of new clauses can be inferred~.5"y.5"y/8 Pb  ` f3|` 3f3` ___>?" dd@,?lPd@ d " @ `"  n?" dd@   @@``@n?" dd@  @@``PV    @ ` ` p>>$ ICCAD'01  03(  0 0 Z?d @?R 0 s *?a j 0 Bv2 @?PP  0 Z?'d @? 0 N gֳgֳ ?"  T Click to edit Master title style! !. 0 HT!gֳgֳ ?*  RClick to edit Master text styles Second level Third level Fourth level Fifth level!     S 0 T!gֳgֳ ?0`P  Y*  0 T"gֳgֳ ?0P  D [*  0 Tt"gֳgֳ ?0 P D [*f 0 Nvd޽h @? ? f3| >Project Overview (Standard).pot $ ICCAD'01 ` 4z(  4 4 Z? @? 4 Z?'d @? 4 NT~Fgֳgֳ ?R" F T Click to edit Master title style! ! 4 HFgֳgֳ ? p F W#Click to edit Master subtitle style$ $ 4 TtFgֳgֳ ?0`P F Y* 4 TFgֳgֳ ?0P  F [* 4 T4Fgֳgֳ ?0 P F [*R  4 s *? f 4 Nv޽h @? ? f3| 0 [S@(  A  Zt|Fxaxa1 ? @ D SClick to edit Master notes styles Second Level Third Level Fourth Level Fifth Level"     Tp  01 ?   DB  s *޽h ? a( 0 0(   B  s *޽h ? a( LDP (  r  S F4" F   HFgֳgֳ ?G     S ~F  g ?=z j"SAT 02, May, 2002 l   C F4 p F H  0޽h ? 3eX{IZ(a  pT$( Ow@ Tr T S 4F0"t  F r T S F0* F H T 0޽h ? f3|  D( w l  C F0"  F   C TF0*<$ 0 F H  0޽h ? f3|<  |( w   S F0"<$ 0  F   S tF0*<$ 0 F H  0޽h ? f3|   ( A`Pp l  C 0"  F l  C '0*M F   S ~'  g ?lt[ ,$D 0 j = (a + c)(b + c)(d + c)(a + b + c) j = (a c)(b c)(d c)(a b c)\(<+H  0޽h ? f3|  ( ? l  C $*0"  F l  C *0* F H  0޽h ? f3|  ,( w x  c $)0  F 9  S ~*  g ? ,$D 0 WBacktrack search (DPLL)$:  S ~+  g ?! 7 ,$D 0 XResolution (original DP)$h  S ~d,  g ?d $ ,$D 0 .Stalmarck s method (SM)"  7  S ~$-  g ? -` ,$D 0 URecursive learning (RL)",  S ~-  g ? ?,$D 0 JBDDs   S ~-  g ?, ,$D  0 9...2   S ~.  g ?P ,$D  0 PLocal search (hill climbing)z Yj D   % P ,$D  0   S ~d/  g ?Yj *  KContinuous formulations   S ~$0  g ?Y p  FGenetic algorithms   S ~0  g ?Y   GSimulated annealing  S ~D1  g ?YD 9...  S ~2  g ?Y= Y Tabu search  .2  C x2g ?-U,$D 0 RSAT Algorithms(fz c~  c~,$D 02  3 rtFg ?cl~ LComplete( f2  C x4g ?k} N Incomplete(  fB B C xDg ?6 hB  3 rDg ?6 mz m% 6   d- ,$D 0*  S ~  g ?m%   tCan prove unsatisfiability$ -  S ~  g ? % 6  wCannot prove unsatisfiability$ H  0޽h ? f3|   ,D( P ,l , C t0"6     , C ԟ0*<$ 0  H , 0޽h ? f3|L  ( x./ l  C 40"   l  C 0*   l  C 0*p   H  0޽h ? f3|  ( w l  C T0"   r  S 0*  H  0޽h ? f3|  D( F8F  Dl D C Ԣ0"   l D C 40*  H D 0޽h ? f3|  H( p Hl H C T0"   l H C 0*  H H 0޽h ? f3|   P( \@ a@ Pl P C t0"  F l P C ԥ0* F H P 0޽h ? f3|  zr0 d ( w dx d c $0"    d c $T0*v <$ 0    d S ~  g ?  ,$D 0 ''j = (a + c)(b + c)(d + c)(a + b + c)(D d S ~)  g ? { ,$D 0 bEliminate variable c2 d S ~O  g ?3 ,$D 0 j1 = (a + a + b)(b + a + b )(d + a + b ) = (d + a + b )HA @@A d S ~dP  g ??{,$D 0 _Instance is SAT !2 z pK 7 W  d  p7 ,$D 0  d c R    BC DEF  @  jJ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| +F  @pK 7 W   d c R    BCDEF  @  jJ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||g< @ 1 T   d c R    BxCoDEF  @  jJ 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||o$xl @ . W H d 0޽h ? f3|  }@h( < hx h c $Q0<,    h S Q0*<$ 0  : h S ~R  g ?p0 ,$D 0 X Try a = 0:2  h S ~dS  g ?p 0 ,$D 0 6(a = 0) (b = 1) (d = 1): h S ~$T  g ?  ,$D 0 X Try a = 1:2  h S ~T  g ?  ,$D  0 6(a = 1) (c = 1) (d = 1) h S ~U  g ?pA 0 ,$D 0  C(a = 0) = {a = 0, b = 1, d = 1}!  h S ~dV  g ? A  ,$D  0  C(a = 1) = {a = 1, c = 1, d = 1}!  h S ~$W  g ?Q  ,$D  0 :C(a = 0) C(a = 1) = {d = 1}  h S ~W  g ?Q  ,$D  0 TAny assignment to variable a implies d = 1. Hence, d = 1 is a necessary assignment !U     sz Z  h Z,$D 0  h # lffg ?ZE h S ~DX  g ?b",$D 0 [#Recursion can be of arbitrary depth$$  h S ~Y  g ?(,$D 0 >$j = (a + b)(a + c) (b + d)(c + d)%J h S ~Y  g ?(,$D 0 h$j = (a + b)(a + c) (b + d)(c + d)(% h S ~Z  g ?(,$D 0 $j = (a + b)(a + c) (b + d)(c + d)%J h S ~D[  g ?(,$D  0 h$j = (a + b)(a + c) (b + d)(c + d)(%H h 0޽h ? f3|{  +#Pl( ޽h lr l S D0"    l S ~  g ?f>L,$D 0 $j = (a + b)(a + c) (b + d)(c + d)%z `  l F,$D 0% l S ~d  g ?In  o(b + c)L l S ~$  g ?s B resolution  B l C xDg ?=iq B lB C xDg ?a ` z c   l I v ,$D 0B  l C xDg ?S  B  lB C xDg ? c %  l S ~  g ?   o(c + d)L  l S ~D  g ?1 m  B resolution  u l S ~  g ? ,$D 0 OComment: SM provides a mechanism for identifying suitable resolution operations(PIz  j l P ,$D 0  l S ~  g ?  W(d)8B l C xDg ?  B l C xDg ?Fj+  l S ~  g ? @ @ resolution g l S ~$  g ? ,$D 0 CSequence of resolution operations for finding necessary assignments&DCH l 0޽h ? f3|x  ( `p(  psz Z p Z,$D 0 p # lffg ?ZE p S ~D  g ?b",$D 0 [#Recursion can be of arbitrary depth$$r p S 0    p S 0*=<$ 0  : p S ~  g ?p0 ,$D 0 X Try a = 1:2  p S ~  g ?,$D 0 "8j = (a + b)(a + d) (b + d)  p S ~D  g ?p 0 ,$D 0 "(a = 1) (d = 1)d:  p S ~  g ?  ,$D 0 X Try b = 1:2   p S ~  g ?  ,$D  0 "(b = 1) (d = 1)d  p S ~  g ?p 0 ,$D 0 C(a = 1) = {a = 1, d = 1}  p S ~P  g ?  ,$D  0 C(b = 1) = {b = 1, d = 1} p S ~  g ?Q  ,$D  0 :C(a = 1) C(b = 1) = {d = 1} p C xf  g ?  ,$D  0 =WEvery way of satisfying (a + b) implies d = 1. Hence, d = 1 is a necessary assignment !X      p S ~g  g ?,$D 0 08j = (a + b)(a + d) (b + d) p S ~Dh  g ?,$D 0 8j = (a + b)(a + d) (b + d) p S ~i  g ?,$D  0 $8j = (a + b)(a + d) (b + d)H p 0޽h ? f3|O    p ( w r  S $j0"     S ~j  g ?E8e,$D 0 8j = (a + b)(a + d) (b + d)z R p  _< },$D 0%  S ~Dk  g ?Iy p o(b + d)L  S ~l  g ?}= B resolution  B  C xDg ?7 Rq B B C xDg ?a V z f(    sV5 ,$D 0B   C xDg ?S V 6 B  B C xDg ? fD    C xdl  g ? B (  W(d)8   C x$m  g ?  B resolution  g  S ~m  g ?+ rk ,$D 0 CSequence of resolution operations for finding necessary assignments&DC  S ~m  g ? ,$D 0 ZComment: RL provides yet another mechanism for identifying suitable resolution operations([TH  0޽h ? f3|  V(  x  c $i0"     S Dn0*<$ 0  H  0޽h ? f3|~  .&( $$ l  C do0"   r  S o0*     C $p0*p <$ 0  H  0޽h ? f3|  L( FF Ll L C p0"   l L C p0*  H L 0޽h ? f3|  ( /@ l  C q0"   l  C r0*  H  0޽h ? f3|  X( w Xl X C 0"   l X C t0*   H X 0޽h ? f3|  PH ( -*` l  C 40"   l  C 0      c A 3?  g ?5  3H  0޽h ? f3|  (  l  C 0"   l  C T0*  H  0޽h ? f3|  PH(  l  C 0"   l  C t0 t    c A 4?  g ?%!>  4H  0޽h ? f3|F    \( w \l \ C 0"    l \ C 40*  l   \,$D 02 \ S ~  Ԕ?"  \ C x  g ?O  0For both assignments to a, a, 0 and a, 1 , we obtain b, 1. \b, 1 is a necessary assignment8eC! e \ S T    B C5DEF  A@  o 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E|| )OZy5@    \ c A 5?  g ?#@ 5H \ 0޽h ? f3|     ^ ( P l  C 0"   l  C T0*  vl 2 ` 2 `,$D 0  C x  g ? ` fEvery assignment that satisfies (b d), also implies c, 0. \c, 0 is a necessary assignmentjb! "a@ d2   d2 2  S ~  o?2  $ 2  S ~  o? 2  S ~  o?5 ' 2   S ~  o?@ d X  d XB  B S ~Do?l U B   S ~Do?dN X  c A 6?  g ?U'D 6H  0޽h ? f3|    ~   ( ~@K@ l  C t0"   l  C 0*U     c A ?  g ?#@ "l  tM  t M ,$D 02  S ~  o? tr2  S ~  o?a~  C N    B CDEF  A@  o 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||_.\ v 0@     C x4  g ? M  One of these assignments must hold (because of a) \ create clause (b c)4L2KH  0޽h ? f3|     0  (  l  C 0"   l  C 0*5    c A ?  g ?#@z  $l r r,$D 02  S ~  o?  2  S ~  o?d  C xT  g ?r r Assume clause w = (a b c) exists. Each assignment that satisfies w implies either c, 0 or d, 0 \ create clause (c d))! 2   S ~  o? B  B S ~Do? jy B  B S ~Do?o t B  B S ~Do?M  H  0޽h ? f3|4  @  d( FPp  l  C t 0"   l  C  0*    c A ?  g ?L-  |l % :  % :,$D 02  c   o?  2  c   o?%xe  S ~4   g ? : fThe assignments a, 0 and b, 1 imply the assignments c, 0 and c, 1; \are disallowed \ create clause (a b)PtJ tB B S ~Do? B  B S ~Do?  H  0޽h ? f3|"  P `b( w `l ` C 0"   l ` C  0*   ` c A ?  g ?L-  zl %"  `%",$D 02 ` S ~  o? G 2 ` S ~  o?%xe2 ` C x   g ? " Assume clause w = (c d) exists. The assignments a, 0 or b, 0 unsatisfy w. \ create clause (a b)h hB  `B C xDo? B  `B C xDo? H ` 0޽h ? f3|  `<( C4P  <l < C  0"   l < C di0*  H < 0޽h ? f3|  p( `P`| l  C T 0"   l  C  0*  H  0޽h ? f3|  (D( ., (l ( C 0"    ( C 40*<$ 0  H ( 0޽h ? f3|  <4 ( w r  S 0"   r  S 0*  l 1Tp  T1p,$D 0~  C N    B+CDEF  A@  o 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||>` +@  W="   S ~t  g ?a@ ZO(L N)~  C N    BJCDEF  A@  o 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||awJ@  _= \ #  C x4  g ? R sCan loop O(N) times&~   C N    BC DEF  A@  o 8c8c     ?1 d0u0@Ty2 NP'p<'pA)BCD|E||qax$ @  1TO   S ~  g ?up 'Polynomial time if depth is constant ! 8(%'H  0޽h ? f3|  xD( p xl x C t0"    x C 0*<$ 0  H x 0޽h ? f3|  ( ., l  C 0"   l  C 0*  H  0޽h ? f3|  (  l  C 0"   l  C 0*  H  0޽h ? f3|  (  l  C 40"   l  C 0*  H  0޽h ? f3|  (  l  C T0"   l  C 0*>  H  0޽h ? f3|  (  l  C O0"   l  C O0*  H  0޽h ? f3|  (  l  C Q0"   l  C tQ0*  H  0޽h ? f3|  ( K@~@ l  C Q0"   l  C 4R0*  H  0޽h ? f3|   ( i _@_ l  C R0"   l  C R0*