Stochastic satisfiability (SSAT) is an extension of satisfiability (SAT) that merges two important areas of artificial intelligence: logic and probabilistic reasoning. Initially suggested by Papadimitriou, who called it a “game against nature”, SSAT is interesting both from a theoretical perspective–it is complete for PSPACE, an important complexity class–and from a practical perspective–a broad class of probabilistic planning problems can be encoded and solved as SSAT instances. This chapter describes SSAT and its variants, their computational complexity, applications of SSAT, analytical results, algorithms and empirical results, related work, and directions for future work.

This paper describes Swarm Performance and Improvisation (Swarm-PI), a real-time computer environment for music improvisation that uses swarm algorithms to control sound synthesis and to mediate interactions with a human performer. Swarm models are artificial, multi-agent systems where the organized movements of large groups are the result of simple, local rules between individuals. Swarms typically exhibit self-organization and emergent behavior. In Swarm-PI, multiple acoustic descriptors from a live audio feed generate parameters for an independent swarm among multiple swarms in the same space, and each swarm is used to synthesize a stream of sound using granular sampling. This environment demonstrates the effectiveness of using swarms to model human interactions typical to group improvisation and to generate organized patterns of synthesized sound.

The expenseMajercik, S. of evaluating the function to be optimized can make it difficult to apply the Particle Swarm Optimization (PSO) algorithm in the real world. Approximating the function is one way to address this issue, but an alternative is conservation of function evaluations. GREEN-PSO (GR-PSO) adopts the latter approach: given a fixed number of function evaluations, GR-PSO conserves them by probabilistically choosing a subset of particles smaller than the entire swarm on each iteration and allowing only those particles to perform function evaluations. Since fewer function evaluations are used on each iteration, the algorithm can use more particles and/or more iterations for a given number of function evaluations. GR-PSO has been shown to be effective using the global topology, performing as well as, or better than, the standard PSO algorithm (S-PSO) [7]. We extend these results by showing that GR-PSO can achieve significantly better performance than S-PSO, in terms of both best function value achieved and rate of error reduction, using three other topologies—ring, von Neumann, and Moore—on a set of six standard benchmark functions, and that the von Neumann and Moore topologies can be more effective topologies for GR-PSO than the global topology.

Fluid Neural Networks (FNNs) are a model of interacting mobile automata. The automata move on a lattice, affecting each other's motion in a way that can result in clusters of automata that change over time, making FNNs a potential basis for dynamic neighborhood topologies in Particle Swarm Optimization. We describe Fluid Neural Network Particle Swarm Optimization (FNN-PSO), a PSO algorithm that uses a dynamic neighborhood mechanism based on FNNs, and we report promising results from experiments indicating that FNN-PSO can outperform both the standard PSO algorithm and PCGT-PSO, a PSO algorithm based on partially connected grid topologies [3], over a range of neighborhood topologies and influence models.

In the Particle Swarm Optimization (PSO) algorithm, the expense of evaluating the objective function can make it difficult, or impossible, to use this approach effectively; reducing the number of necessary function evaluations would make it possible to apply the PSO algorithm more widely. Many function approximation techniques have been developed that address this issue, but an alternative to function approximation is function conservation. We describe GREEN-PSO (GR-PSO), an algorithm that, given a fixed number of function evaluations, conserves those function evaluations by probabilistically choosing a subset of particles smaller than the entire swarm on each iteration and allowing only those particles to perform function evaluations. The “surplus” of function evaluations thus created allows a greater number of particles and/or iterations. In spite of the loss of information resulting from this more parsimonious use of function evaluations, GR-PSO performs as well as, or better than, the standard PSO algorithm on a set of six benchmark functions, both in terms of the rate of error reduction and the quality of the final solution.

Swarm intelligence can provide robust, adaptable, scalable solutions to difficult problems. The distributed nature of swarm activity is the basis of these desirable qualities, but it also prevents swarm-based techniques from having direct access to global knowledge that could facilitate the task at hand. Our experiments indicate that a swarm system can use an auxiliary swarm, called a communication swarm, to create and distribute an approximation of useful global knowledge, without sacrificing robustness, adaptability, and scalability. We describe a communication swarm and validate its effectiveness on a simple problem.

Swarm intelligence is a natural phenomenon in which complex behavior emerges from the collective activities of a large number of simple individuals. Swarms are adaptable to changes in their environments, robust to the loss of swarm members, and scalable. Swarm algorithms attempt to capture these desirable qualities by distributing computation among simple agents that interact and sense only locally, the desired solution or behavior emerging from their actions. We introduce Swarm Search-and-Rescue (swarm-sr), a swarm algorithm that locates survivors in a dynamic, hazardous environment, finds high quality paths from an arbitrary starting location to these survivors, physically marks the paths so that they can be traversed by human rescuers, and updates the paths, creating new paths if necessary, to reflect changing conditions. We present results of successful initial tests of swarm-sr in a simulated disaster scenario.

zander is a state-of-the-art probabilistic planner that extends the probabilistic-planning-as-stochastic-satisfiability paradigm to support contingent planning in domains where there is uncertainty in the effects of the agent’s actions and where the scope and accuracy of the agent’s observations may be insufficient to establish the agent’s current state with certainty (Majercik & Littman 1999). We describe zander and then discuss an approximation technique we are developing that will help us to scale up our SSat-based technique to large planning problems. We report results using this approximation algorithm on random SSat problems and discuss issues that arise in the application of this algorithm to SSat encodings of planning problems.

We describe APPSSAT, an approximate probabilistic contingent planner based on ZANDER, a probabilistic contingent planner that operates by converting the planning problem to a stochastic satisfiability (Ssat) problem and solving that problem instead [1]. The values of some of the variables in an Ssat instance are probabilistically determined; APPSSAT considers the most likely instantiations of these variables (the most probable situations facing the agent) and attempts to construct an approximation of the optimal plan that succeeds under those circumstances, improving that plan as time permits. Given more time, less likely instantiations/situations are considered and the plan is revised as necessary. In some cases, a plan constructed to address a relatively low percentage of possible situations will succeed for situations not explicitly considered as well, and may return an optimal or near-optimal plan. This means that APPSSAT can sometimes find optimal plans faster than ZANDER. And the anytime quality of APPSSAT means that suboptimal plans could be efficiently derived in larger time-critical domains in which ZANDER might not have sufficient time to calculate the optimal plan. We describe some preliminary experimental results and suggest further work needed to bring APPSSAT closer to attacking real-world problems.

We present DC-SSAT, a sound and complete divide-and-conquer algorithm for solving stochastic satisfiability (SSAT) problems that outperforms the best existing algorithm for solving such problems (ZANDER) by several orders of magnitude with respect to both time and space. DC-SSAT achieves this performance by dividing the SSAT problem into subproblems based on the structure of the original instance, caching the viable partial assignments (VPAs) generated by solving these subproblems, and using these VPAs to construct the solution to the original problem. DC-SSAT does not save redundant VPAs and each VPA saved is necessary to construct the solution. Furthermore, DC-SSAT builds a solution that is already human-comprehensible, allowing it to avoid the costly solution rebuilding phase in ZANDER. As a result, DC-SSAT is able to solve problems using, typically, 1-2 orders of magnitude less space than ZANDER, allowing DC-SSAT to solve problems ZANDER cannot solve due to space constraints. And, in spite of its more parsimonious use of space, DCSSAT is typically 1-2 orders of magnitude faster than ZANDER. We describe the DC-SSAT algorithm and present empirical results comparing its performance to that of ZANDER on a set of SSAT problems.

The propositional contingent planner ZANDER solves finite-horizon, partially observable, probabilistic planning problems at state-of-the-art-speeds by converting the planning problem to a stochastic satisfiability (SSAT) problem and solving that problem instead (Majercik 2000). ZANDER obtains these results using a relatively inefficient SSAT encoding of the problem (a linear action encoding with classical frame axioms). We describe and analyze three alternative SSAT encodings for probabilistic planning problems: a linear action encoding with simple explanatory frame axioms, a linear action encoding with complex explanatory frame axioms, and a parallel action encoding. Results on a suite of test problems indicate that linear action encodings with simple explanatory frame axioms and parallel action encodings show particular promise, improving ZANDER's efficiency by as much as three orders of magnitude.

We describe two new probabilistic planning tech-niques|c-maxplan and zander|that generate con-tingent plans in probabilistic propositional domains. Both operate by transforming the planning problem into a stochastic satis ability problem and solving that problem instead. c-maxplan encodes the problem as an E-Majsat instance, while zander encodes the problem as an S-Sat instance. Although S-Sat prob-lems are in a higher complexity class than E-Majsat problems, the problem encodings produced by zander are substantially more compact and appear to be easier to solve than the corresponding E-Majsat encodings. Preliminary results for zander indicate that it is com-petitive with existing planners on a variety of problems.

Satisfiability problems and probabilistic models are core topics of artificial intelligence and computer science. This paper looks at the rich intersection between these two areas, opening the door for the use of satisfiability approaches in probabilistic domains. The paper examines a generic stochastic satisfiability problem, SSAT, which can function for probabilistic domains as SAT does for deterministic domains. It shows the connection between SSAT and well-studied problems in belief network inference and planning under uncertainty, and defines algorithms, both systematic and stochastic, for solving SSAT instances. These algorithms are validated on random SSAT formulae generated under the fixed-clause model. In spite of the large complexity gap between SSAT (PSPACE) and SAT (NP), the paper suggests that much of what we have learned about SAT transfers to the probabilistic domain.

C-MAXPLAN extends MAXPLAN to include contingent planning in probabilistic propositional domains. Like MAXPLAN, C-MAXPLAN converts the planning problem into an E-MAJSAT instance, a type of probabilistic satisfiability problem in which a set of Boolean variables encodes the plan and a second set of Boolean variables encodes the probabilistic outcome of the planthe satisfiability problem is to find the setting of the plan variables that maximizes the probability of satisfaction with respect to the outcome variables. We describe two different encodings for contingent plans in this framework: the first one explicitly encodes contingent actions and is similar to the approach taken by C-BURIDAN; the second encodes a policy rather than a plan. Although the efficiency with which the resulting satisfiability problem is solved depends critically on the contingent-plan representation, C-MAXPLAN is competitive with state-of-the-art contingent planners on some problems.

We describe a new planning technique that efficiently solves probabilistic propositional contingent planning problems by converting them into instances of stochastic satisfiability (SSat) and solving these problems instead. We make fundamental contributions in two areas: the solution of SSat problems and the solution of stochastic planning problems. This is the first work extending the planning-as-satisfiability paradigm to stochastic domains. Our planner, zander, can solve arbitrary, goal-oriented, finite-horizon partially observable Markov decision processes (pomdps). An empirical study comparing zander to seven other leading planners shows that its performance is competitive on a range of problems.

Classical artificial intelligence planning techniques can operate in large domains but traditionally assume a deterministic universe. Operations research planning techniques can operate in probabilistic domains but break when the domains approach realistic sizes, MAX-PLAN is a new probabilistic planning technique that aims at combining the best of these two worlds, MAX-PLAN converts a planning instance into an E-MAJSAT instance, and then draws on techniques from Boolean satisfiability and dynamic programming to solve the E-MAJSAT instance. E-MAJSAT is an NPPP-complete problem that is essentially a probabilistic version of SAT. MAXPLAN performs as much as an order of magnitude better on some standard stochastic test problems than BURIDAN—a state-of-the-art probabilistic planner—and scales better on one test problem than two algorithms based on dynamic programming.

Probabilistic planning algorithms seek effective plans for large, stochastic domains. MAXPLAN is a recently developed algorithm that converts a planning problem into an E-MAJSAT problem, an NPPP-complete problem that is essentially a probabilistic version of SAT, and draws on techniques from Boolean satisfiability and dynamic programming to solve the E-MAJSAT problem. This solution method is able to solve planning problems at state-of-the-art speeds, but it depends on the ability to store a value for each CNF subformula encountered in the solution process and is therefore quite memory intensive; searching for moderate-size plans even on simple problems can exhaust memory. This paper presents two techniques, based on caching, that overcome this problem without significant performance degradation. The first technique uses an LRU cache to store a fixed number of subformula values. The second technique uses a heuristic based on a measure of subformula difficulty to selectively save the values of only those subformulas whose values are sufficiently difficult to compute and are likely to be reused later in the solution process. We report results for both techniques on a stochastic test problem.

Our research area is planning under uncertainty, that is, making sequences of decisions in the face of imperfect information. We are particularly concerned with developing planning algorithms that perform well in large, real-world domains. This paper is a brief introduction to this area of research, which draws upon results from operations research (Markov decision processes), machine learning (reinforcement learning), and artiicial intelligence (planning). Although techniques for planning under uncertainty are extremely promising for tackling real-world problems, there is a real need at this stage to look at large-scale applications to provide direction to future development and analysis.

Load balancing is a difficult problem whose solution cangreatly increase the speedup one achieves in a paralleldistributed memory environment. The necessity forload balancing can arise not only from the structureor dynamics of one's problem, but from the need tocompete for processor time with other users. Givena lengthy computation, the ability to exploit changesin processor loads when allocating work or decidingwhether to reallocate work is critical in making the computation...