1、1,Compute-Intensive Methods in AI: New Opportunities for Reasoning and Search Bart Selman Cornell University selmancs.cornell.edu,2,Introduction,In recent years, weve seen substantial progress inpropositional reasoning and search methods.Boolean satisfiability testing:1990: 100 variables / 200 claus
2、es (constraints)1998: 10,000 - 100,000 vars / 106 clausesNovel applications:e.g. in planning, software / circuit testing, machine learning, and protein folding,3,Factors in Progress,a) new algorithms e.g. stochastic methodsb) better implementations several competitions -Germany 91 / China 96 / DIMAC
3、S-93/97/98c) faster hardwareAlso, close interplay between theoretical, experimental,and applied work.,4,Applications: Methodology,CombinatorialTask SAT Encoding SAT Solver DecoderShift work to “encoding phase,use fast, off-the-shelf SAT solver and tools.,5,Compare methodology to the use of Linear /
4、Integer Programming packages:- Emphasis is on mathematical modeling (e.g. using primal and dual formulations).- After modeling phase, problem is handed to a state-of-the-art solver.,6,Perhaps theoretically, but often not in practice- Its difficult to duplicate efforts put in designingfast solvers.-
5、Encodings can compensate for much of theloss due to going to a uniform representationformalism (e.g. SAT, CSP, LP, or MIP).,Would specialized solver not be better?,7,Outline,I - Example application: AI PlanningThe SATPLAN systemII - Current Themes in SAT Solversrandomization / scalabilityIII - Curre
6、nt Themes in SAT Encodingsdeclarative control knowledgeIV - Conclusions,8,I. Example Application: Planning,9,Planning: find a (partially) ordered set of actions that transform a given initial state to a specified goal state.in most general case, can cover most forms of problem solving special case o
7、f program synthesis scheduling: fixes set of actions, need to find optimal total ordering- planning problems typically highly non-linear, require combinatorial search,10,Some Applications of Planning,Autonomous systemsDeep Space One Remote Agent (NASA) mission planning Softbots - software robots Int
8、ernet agents, program assistants AI “characters” in games, entertainment Synthesis, bug-finding (goal = undesirable state), Supply Chain Management - “just-in-time” manufacturing (SAP, I2, PeopleSoft etc. $10 billion) Proof planning in mathematical domains (Melis 1998),11,State-space Planning,Find a
9、 sequence of operators that transform an initial state to a goal stateState = complete truth assignment to a set of variables (fluents) Goal = partial truth assignment (set of states)Operator = a partial function State State specified by three sets of variables:precondition, add list, delete list(ST
10、RIPS-style, Nilsson & Fikes 1971),12,Abdundance of Negative Complexity Results,I. Domain-independent planning: PSPACE-complete or worse (Chapman 1987; Bylander 1991; Backstrom 1993)II. Domain-dependent planning: NP-complete or worse (Chenoweth 1991; Gupta and Nau 1992)III. Approximate planning: NP-c
11、omplete or worse (Selman 1994),13,Practice,Traditional domain-independent planners can generate plans of only a few steps. Prodigy, Nonlin, UCPOP, . Practical systems minimize or eliminate search by employing complex search control rules, hand-tailored to the search engine and the particular search
12、space (Sacerdoti 1975, Slaney 1996, Bacchus 1996) pre-compiling entire state-space to a reactive finite-state machine (Agre & Chapman 1997, Williams & Nayak 1997) Scaling remains problematic when state space is large or not well understood!,14,Progression,Planning as first-order theorem proving (Gre
13、en 1969) computationally infeasibleSTRIPS (Fikes & Nilsson 1971) very hardPartial-order planning (Tate 1977, McAllester 1991, Smith & Peot 1993) can be more efficient, but still hard (Minton, Bresina, & Drummond 1994)Proposal: planning as propositional reasoning,15,Approach,SAT encodings are designe
14、d so that plans correspond to satisfying assignmentsUse recent efficient satisfiability procedures (systematic and stochastic) to solveEvaluation performance on benchmark instances,16,SATPLAN,axiom schemas,instantiated propositional clauses,satisfying model,plan,mapping,length,problem description,SA
15、T engine(s),instantiate,interpret,17,SAT Encodings,Propositional CNF: no variables or quantifiers Sets of clauses specified by axiom schemas fully instantiated before problem-solving Discrete time, modeled by integers state predicates: indexed by time at which they hold action predicates: indexed by
16、 time at which action begins each action takes 1 time step many actions may occur at the same step fly(Plane, City1, City2, i) at(Plane, City2, i +1),18,Solution to a Planning Problem,A solution is specified by any model (satisfying truth assignment) of the conjunction of the axioms describing the i
17、nitial state, goal state, and operatorsEasy to convert back to a STRIPS-style plan,19,Satisfiability Testing Procedures,Systematic, complete procedures Depth-first backtrack search (Davis, Putnam, & Loveland 1961) unit propagation, shortest clause heuristic State-of-the-art implementation: ntab (Cra
18、wford & Auton 1997) and many others! See SATLIB 1998 / Hoos & Stutzle.Stochastic, incomplete procedures GSAT (Selman et. al 1993) Current fastest: Walksat (Selman & Kautz 1993) greedy local search + noise to escape local minima,20,Walksat Procedure,Start with random initial assignment. Pick a random
19、 unsatisfied clause. Select and flip a variable from that clause: With probability p, pick a random variable. With probability 1-p, pick greedily a variable that minimizes the number of unsatisfied clauses Repeat to predefined maximum number flips; if no solution found, restart.,21,Planning Benchmar
20、k Test Set,Extension of Graphplan benchmark set Graphplan faster than UCPOP (Weld 1992) and Prodigy (Carbonell 1992) on blocks world and rocket domains logistics - complex, highly-parallel transportation domain, ranging up to 14 time slots, unlimited parallelism 2,165 possible actions per time slot
21、optimal solutions containing 150 distinct actions Problems of this size (1018 configurations) not previously handled by any state-space planning system,22,Solution of Logistics Problems,0.01,0.1,1,10,100,1000,10000,100000,rocket.a,rocket.b,log.a,log.b,log.c,log.d,log solution time,Graphplan,ntab,wal
22、ksat,23,What SATPLAN Shows,A general propositional theorem prover can be competitive with specialized planning systemsSurpise:“Search direction” does not appear to matter. (Traditional planners generallybackward chain from goal state.)Fast SAT engines stochastic search - walksat large SAT/CSP commun
23、ity sharing ideas and code specialized engines can catch up, but by then, new general technique,24,II. Current Themes in Sat Solvers,25,SAT Solvers,Stochastic local search solvers (walksat) when they work, scale well cannot show unsat fail on certain domains must use very simple (fast) heuristics Sy
24、stematic solvers (Davis Putnam Loveland style) complete fail on (often different) domains might use more sophisticated (costly) heuristics often to scale badly Can we combine best features of each approach?,26,Background,Combinatorial search methods often exhibita remarkable variability in performan
25、ce. It iscommon to observe significant differencesbetween:- different heuristics- same heuristic on different instances- different runs of same heuristic with different seeds (stochastic methods),27,Preview of Strategy,Well put variability / unpredictability to our advantage via randomization / aver
26、aging.,28,Cost Distributions,Backtrack-style search (e.g. Davis-Putnam) characterized by:I Erratic behavior of mean.II Distributions have “heavy tails”.,29,30,31,32,Heavy-Tailed Distributions, infinite variance infinite meanIntroduced by Pareto in the 1920s - “probabilistic curiosity.”Mandelbrot est
27、ablished the use of heavy-tailed distributions to model real-world fractal phenomena.Examples: stock-market, earth-quakes, weather,.,33,Decay of Distributions,Standard - Exponential Decaye.g. Normal:Heavy-Tailed - Power Law Decaye.g. Pareto-Levy:,34,Standard Distribution (finite mean & variance),Pow
28、er Law Decay,Exponential Decay,35,How to Check for “Heavy Tails”?,Log-Log plot of tail of distribution should be approximately linear.Slope gives value of infinite mean and infinite varianceinfinite variance,36,37,38,Heavy Tails,Bad scaling of systematic solvers can be caused by heavy tailed distrib
29、utionsDeterministic algorithms get stuck on particular instances but that same instance might be easy for a different deterministic algorithm!Expected (mean) solution time increases without limit over large distributions,39,Randomized Restarts,Solution: randomize the systematic solver Add noise to t
30、he heuristic branching (variable choice) function Cutoff and restart search after a fixed number of backtracksProvably Eliminates heavy tailsIn practice: rapid restarts with low cutoff can dramatically improve performance(Gomes and Selman 1997, 1998),40,Rapid Restart on LOG.D,Note Log Scale: Exponen
31、tial speedup!,41,SATPLAN Results,42,Overall insight: Randomized tie-breaking with rapid restarts gives powerful bactrack-style search strategy. (sequential / interleaved / parallel)Related analysis: Luby Alt & Karp 1996.,43,Heavy-Tailed Distributions in Other Domains,Quasigroup Completion ProblemGra
32、ph ColoringLogistic PlanningCircuit Synthesis,44,Deterministic,(*) not found after 2 days,Sample Results Random Restarts,Gomes, Kautz, Selman 1998,45,SAT Solvers: Themes, cont.,Randomization (as discussed)Hybrid solvers - Algorithm Portfolios(Hogg Gomes & Selman 1997)Using LP relaxations (Warners &
33、van Maaren 1998)Between 2SAT / 3SAT: Mixture can behave as pure 2SAT!(Kirkpatrick, Selman, et al. 1996 / 1998),46,47,48,SAT Solvers: Recent Theory,Minimal size of search tree (Beame, Karp, et al. 1998)Better worst-case: less than O(2n)backtrack style: O(2(0.387n)(Schiermeyer 1997; Paturi, et al. 199
34、8)local search: O(2(c.n) with c 1(Hirsch, 1998),49,IV. Current Themes in Encodings,50,Add Declarative Domain Knowledge,Efficient representations and (randomized) SAT engines extend the range of domain-independent planningWays for further improvement: Better general search algorithms Incorporate (mor
35、e) domain dependent knowledge,51,Kinds of Knowledge,* About domain itself a truck is only in one location airplanes are always at some airport * About good plans do not remove a package from its destination location do not unload a package and immediate load it again X About how to search plan air r
36、outes before land routes work on hardest goals first,52,Expressing Knowledge,Such information is traditionally incorporated in the planning algorithm itself or in a special programming language Instead: use additional declarative axiomsProblem instance: operator axioms + initial and goal axioms + he
37、uristic axioms Domain knowledge constraints on search and solution spaces Independent of any search engine strategy,53,Logical Status of Heuristics,1. Entailed by operator axioms: conflicts and derived effects fly(plane,d1,i) and fly(plane,d2,i) conflict 2. Entailed by operators + initial state axio
38、ms: state invariants a truck is at only one location 3. Entailed by operators + initial + goal + length: optimality conditions do not return a package to a location 4. New constraints on problem instance: simplifying assumptions Once a truck is loaded, it should immediately move,54,Axiomatic Form,In
39、variant: A truck is at only one locationat(truck,loc1,i) & loc1 loc2 at(truck,loc2,i) Optimality: Do not return a package to a locationat(pkg,loc,i) & at(pkg,loc,i+1) & ij at(pkg,loc,j) Simplifying: Once a truck is loaded, it should immediately move in(pkg,truck,i) & in(pkg,truck,i+1) & at(truck,loc
40、,i+1) at(truck,loc,i+2),55,Questions,Does it work? Additional axioms might just blow up instance with redundant informationIs effect independent of search engine?Can we predict the most useful level of heuristic axioms? What is relation of difficulty to problem size?,56,Experiment: Logistics,h1: Opt
41、imality conditions Once a package leaves a location, it never returns h2, h3: Simplifying assumptions A package is never in any city other than its origin or destination cities rules out solutions where packages are transferred between airplanes in an intermediate city Once a vehicle is loaded, it s
42、hould immediately move rules out solutions where vehicles are loaded incrementally h4: More optimality conditions A package never leaves its destination city,57,ntab solution of logistics,58,Answers,Does it work? YES, 10 to 100+ times speedupIs effect independent of search engine? YES, same heuristi
43、cs best for systematic and stochastic engines - but needs more investigationCan we predict the most useful level of heuristic axioms? USUALLY point at which problem size is minimized after simplification by unit propagation (40% - 70% reduction),59,How to Generate Control Knowledge - Automatically,P
44、olytime preprocessing Try to add “obvious” inferences (McAllester, Crawford)Compilation Fix operators and initial or goal state, generate tractable equivalent theory (Kautz Koehler & Nebel - IPP system 1998),60,Encodings: Themes cont.,Add declarative control knowledge (as discussed)RobustnessSmall c
45、hange in original formulation, small change in encoding.Add numeric information / “soft constraints”Weighted MAXSAT?More compact encodings.E.g. causal.,61,Conclusions,Discussed current state-of-the-art in propositionalreasoning and search.Shift to 10,000+ variables and 106 clauses hasopened up new a
46、pplications.Methodology: Find compact SAT encoding;Use off-the-shelf SAT Solver.Analogous to LP and MIP approaches.,62,Conclusions, cont.,Example: AI planning / SATPLAN systemOne order of magnitude improvement (last 3yrs):10 step to 200 step plansNeed two more:up to 20,000 step .Discussed themes in SAT Sovers / EncodingsHeavy-tails / Randomization / Declarative domain knowledge,
