a SAT technology planning system
WOW!  Now Supercharged with Chaff!
What's New in Version 42

http://www.cs.rochester.edu/~kautz/satplan/blackbox

DOWNLOAD Blackbox


Looking for SATPLAN-2004?  Then go to the SATPLAN home page instead.  This page is about the 1997-2003  version of our planning as satisfiability system.

Supercharged!

If you think you know blackbox, think again!  Try out the new version that includes the powerful new SAT solver Chaff from Princeton!
 

blackbox = satplan + graphplan

Blackbox is a planning system that works by converting problems specified in STRIPS notation into Boolean satisfiability problems, and then solving the problems with a variety of state-of-the-art satisfiability engines. The front-end employs the graphplan system (Blum and Furst 1995). There is extreme flexibility in specifying the engines to use. For example, you can tell it to use walksat (Selman, Kautz, and Cohen 1994) for 60 seconds, and if that fails, then satz (Li and Anbulagan 1997) for 1000 seconds. This gives blackbox the capability of functioning efficiently over a broad range of problems. The name blackbox refers to the fact that the plan generator knows nothing about the SAT solvers, and the SAT solvers know nothing about plans: each is a "black box" to the other.

Read the paper Unifying SAT-based and Graph-based Planning, Proc. IJCAI-99, Stockholm.

You can also download the original SATPLAN (Kautz and Selman 1992, 1998) system (that uses hand-encoded logical axioms) from the Blackbox Download Page.
 

installing blackbox

Go to the Blackbox Download Page to download source and/or binaries for Linux and MS Windows.

The source should compile under most flavors of Unix (possibly with some minor modifications needed for more exotic varieties).  The primary version of Unix supported is Linux.  The source distribution also includes a directory of Example domains and some documentation.

The Windows version is currently compiled using a Windows/Unix compatibility package called Cygwin.  The download page explains how to obtain and install the runtime libraries used by Cygwin.  It is possible to make minor modifications to the code to compile directly under Windows.  An older version of blackbox that runs without the Cygwin libraries also appears on the download page.
 

using blackbox

The input to blackbox are STRIPS-style problems in PDDL (Planning Domain Definition Language).   To get started, try: Blackbox has many options.   For help type: Blackbox will print the solver schedule, and optionally the wff (in cnf or literal form), the mapping from literals to propositions, the model found, and the plan. The script "extract" can be used to extract the desired piece from the output of blackbox.  For example, the following prints the wff generated by the problem blocks.facts.easy: Performance on the hardest planning problems can be improved by tuning the specific solver parameters, and in particular, the cutoff and noise parameters for walksat, satz, or relsat.  The script Run-bb invokes blackbox inside of a shell that terminates execution when specified CPU memory limits are exceeded.

problem instances

The subdirectory Examples/ contains a small set of problem domains.  The most extensive set of test examples are in Examples/logistics-strips. Here is a solution to log-d , that contains 100 actions.  The script Solve-All can be used to automatically run blackbox on all the instances in a subdirectory.  The PDDL versions of the logistics and blocks world problems used in the papers by Kautz and Selman (1996, 1998) are included.

the PDDL input language

The Planning Domain Definition Language (PDDL) was created by the AIPS-98 Planning Competition Committee, headed by Drew McDermott.  Blackbox (version 2.0) reads this language as specified below.
what's new in version 42!

Version 42 reduces the number of propositions allocated per level so it consumes less memory.  If this keeps your problems from running, use the -M flag.

Version 41 fixes a dump-core bug and compiles under both Linux and Windows using Cygwin.  Blackbox will still crash if it runs out memory.

Version 3.9 fixes bugs in Chaff and adds a Windows binary for Chaff.  There are still some remaining bugs in this version of  Chaff: (1) Chaff sometimes dumps core, especially under Windows; and (2) The Chaff solver does not appear to run as fast as earlier stand-alone Chaff binaries distributed from Princeton.  We are currently working on these issues.

Version 3.8 adds the new SAT solver zchaff and uses it by default.  Only a Linux binary is currently available.

Version 3.7 fixes the Makefiles and function declarations so fewer warnings are issued under g++.

Version 3.6 fixes some bugs in parser and the help screens, and introduces a version for Microsoft Windows.

Version 3.5 updates the satz-rand solver and includes a way to assert control knowledge, as described in the paper "Control Knowledge in Planning: Benefits and Tradeoffs" Proc. AAAI-99. Here is a brief description of the current syntax of the control knowledge language, which is likely to change in the future.

Version 3.4 fixes a bug in some of the earlier released versions of the logistics test examples log.a, log.b, log.c. Some of the versions included in earlier releases of blackbox included objects that were not actually used in the precondition or goal of the plan. These objects did not appear in the original problems derived from SATPLAN and Graphplan, and did not significantly effect the performance of blackbox. However, because they could affect the performance of some solvers, we encourage users to base comparative tests on these corrected versions. The distribution contains four versions of the logistics domain: logistics-strips, logistics-strips-length, logistics-typed, logistics-typed-length, where the "-length" versions specify the minimum parallel length.

Version 3.4 also extends the -axioms option as described below.

Version 3.0 adds the solver rel_sat_rand, a randomized/restart version of the solver rel_sat created by Roberto Bayardo. Rel_sat performs dependency-directed backtracking. It is invoked by the flag -relsat. This version also improves the implementation of the parser.

Version 2.5 fixes a bug that caused some clauses in the generated wff to appear twice, and allows detailed control over the kinds of axioms generated during the translation.   The option -axoms N specifies what kinds of axioms are generated, where N is a sum of the following:

The -axioms flag takes either a numeric argument or one of the following keywords: The Version 2.5 also pretty prints the solution plan; the original format can be printed by using the option -nopretty.

Version 2.0 adds the simplifier compact and reads the input language PDDL (Planning Definition Domain Language), the language of the AIPS-98 planning competition.

Version 1.0 included the solvers graphplan, walksat, and satz_rand.

All versions still do not free up memory once it is allocated, and so may run out of memory on large problems.

credits

bibliography

Yi-Cheng Huang, Bart Selman, and Henry Kautz (2000). Learning Declarative Control Rules for Constraint-Based Planning.Proc. ICML-2000 (Seventeenth International Conference on Machine Learning), Stanford, CA.
Henry Kautz and Bart Selman (1999). Unifying SAT-based and Graph-based Planning.Proc. IJCAI-99.
Yi-Cheng Huang, Bart Selman, and Henry Kautz (1999). Control Knowledge in Planning: Benefits and Tradeoffs. Proc. AAAI-99.
R. J. Bayardo Jr. and R. C. Schrag (1997). Using CSP look-back techniques to solve real world SAT instances. Proc. AAAI-97.
A. Blum and M.L. Furst (1995). Fast planning through planning graph analysis. Proc. IJCAI-95.
M.D. Ernst, T.D. Millstein, and D.S. Weld (1997). Automatic SAT-compilation of planning problems. Proc. IJCAI-97.
Carla P. Gomes and Bart Selman (1997). Problem Structure in the Presence of Perturbations. Proc. AAAI-97.
Carla P. Gomes, Bart Selman, and Henry Kautz (1998). Boosting Combinatorial Search Through Randomization. Proc. AAAI-98.
Yi-Chen Huang, Bart Selman, and Henry Kautz (1999). "Control Knowledge in Planning: Benefits and Tradeoffs" Proc. AAAI-99, Orlando.
Henry Kautz and Bart Selman (1999). Unifying SAT-based and Graph-based Planning. Proc. IJCAI-99, Stockholm.
Henry Kautz and Bart Selman (1992). Planning as Satisfiability. Proc. ECAI-92.
Kautz, H. and Selman, B. (1996). Pushing the Envelope: Planning, Propositional Logic, and Stochastic Search. Proc. AAAI-96.
Henry Kautz and Bart Selman (1998). The Role of Domain-Specific Knowledge in the Planning as Satisfiability Framework. ( Figures.) Proc. AIPS-98, Pittsburgh, PA.
Henry Kautz and Bart Selman (1998). BLACKBOX: A New Approach to the Application of Theorem Proving to Problem Solving. Working notes of the Workshop on Planning as Combinatorial Search, held in conjunction with AIPS-98, Pittsburgh, PA, 1998.
Chu Min Li and Anbulagan (1997). Heuristics based on unit propagation for satisfiability problems. Proc. IJCAI-97.
Drew McDermott and the AIPS-98 Planning Competition Committee.  PDDL - The Planning Domain Definition Language, Draft 1.6, June 1998.
Bart Selman, Hector Levesque and David Mitchell (1992). A New Method for Solving Hard Satisfiability Problems. Proc. AAAI-92.
Bart Selman, Henry Kautz, and Bram Cohen (1994). Noise Strategies for Improving Local Search. Proc. AAAI-94.

Henry Kautz updated 15 January 2003
Home page: http://www.cs.washington.edu/homes/kautz