a SAT technology planning system
WOW!
Now Supercharged with Chaff!
What's
New in Version 42
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:
cd Examples/logistics-strips
blackbox -o domain.pddl -f prob004-log-a.pddl
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:
blackbox -o blocks.ops -f blocks.facts.easy -printcnf -printexit
| extract cnf
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.
-
(:requirements) may include :strips, :equality, and :typing.
-
Blackbox assumes that all parameters to an operator must be bound to different
objects. Therefore, inequality preconditions such as (not (= ?x ?y))
are handled simply by being ignored. Strict equality conditions are
unnecessary (simply use the same variable) and are not handled. Note
that the assumption that parameters are bound apart is not part of the
PDDL definition (but is almost always useful).
-
(:constants) are not always parsed correctly. If you get unexpected
errors in domains including constants, try rewriting the domain so that
they are not used.
-
Negated preconditions (other than equality) are handled by generating new
predicates. For example, a :precondition of (not (at ?x ?y)) is converted
to (not-at ?x ?y), and appropriate additional :effects are added to all
operators. It is necessary to explicitly declare any negative facts
that hold in the initial state that are needed to solve the plan.
Alternatively, the command line flag -n can be used to force Blackbox to
make an explicit closed-world assumption, and add all negative facts to
the initial state (however, this can be inefficient). As a special
case, if negative preconditions appear in some operator and no negative
facts appear in the (:init) part of the instance, then the -n flag is automatically
invoked.
-
Only simple typing information is supported. In operator files, variables
and objects should only have atomic types. The (:types) constructor should
contain only a list of types (do not try to create subtypes or use fluents).
In a fact file, an object can be given several types by use of the (either)
construct:
(:objects lincolncenter
- LOCATION jfk - (either AIRPORT LOCATION))
Do not attempt to use types as unary predicates (as allowed by the
PDDL definition); this will not work.
-
Input in case-insensitive.
-
All (:objects) must be declared in the problem instance.
-
The domain names must match in the operator and problem instance
files.
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:
-
1 = mutex between incompatible actions
-
2 = action implies precondition
-
4 = fact implies disjunction of actions that add (frame axiom)
-
8 = mutex between incompatible facts
-
16 = action implies effect
-
32 = do not prune mutexes between actions that logically follow from other
axioms
-
64 = include duplicate axioms generated by buggy versions 2.0 and earlier
-
128 = include axioms that chain from action to action, bypassing facts
(included in Version 3.4)
The -axioms flag takes either a numeric argument or one of the following
keywords:
-
default = 7 = 1+2+4
-
compressed = 31 = 1+2+4+8+16 (prunes some mutexes)
-
expanded = 63 = 1+2+4+8+16+32
-
action = 129 = 1+128 (only action propositions appear in encoding)
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
-
The overall design and implementation of blackbox, including the routines
that convert planning graphs to formulas and back, was by Henry
Kautz.
-
Henry Kautz and Bart Selman
developed the idea of planning as propositional satisfiability testing
in their work on SATPLAN.
-
The MEDIC system of Dan
Weld, Michael Ernst, and Todd Millstein developed the idea of automatically
generating and solving SAT representations of planning problems specified
in STRIPS-like notation. (No actual code from MEDIC appears in blackbox.)
-
The front-end of blackbox is a modified version of the code of the graphplan
system
of Avrim
Blum and Merrick Furst.
-
The PDDL parser for blackbox was written by Yi-Cheng
Huang, who is currently working on a version of Blackbox that automatically
learns control knowledge.
-
The walksat solver was written by Henry Kautz, Bart Selman, and Bram Cohen.
-
Carla Gomes initiated the idea
of combining randomization and restarts with systematic search procedures
in order to reduce expected solution time.
-
The original satz solver was written by Chu
Min Li and Anbulagan. Blackbox uses a modified version, satz_rand,
that includes the option of performing randomized restarts in order to
decrease the expected solution time.
-
The original rel_sat solver was written by Roberto
Bayardo. Blackbox uses a version modified by Henry Kautz,
rel_sat_rand, that adds noise and a cutoff parameter.
-
The simplifier compact was created by Jimi Crawford.
-
Version 3.6 was ported to Windows by Peter
Bozarov.
-
The SAT solver chaff is a work in progress by Sharad
Malik <sharad@ee.princeton.edu>, Lintao
Zhang <lintaoz@ee.princeton.edu>, Yingzhao, and Matthew Moskewicz
at Princeton University. It is an insanely great systematic SAT engine.
Please contact them for information on obtaining a linkable library for
chaff.
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