Blackbox is a planning system that works by converting problems
in STRIPS notation into Boolean satisfiability problems, and then
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,
can tell it to use walksat (Selman, Kautz, and Cohen 1994) for 60
and if that fails, then satz (Li and Anbulagan 1997) for 1000 seconds.
This gives blackbox the capability of functioning efficiently over a
range of problems. The name blackbox refers to the fact that the plan
knows nothing about the SAT solvers, and the SAT solvers know nothing
plans: each is a "black box" to the other.
a SAT technology planning system:
blackbox = satplan + graphplan
- Download and run the pre-compiled Linux, Mac OS X, or Windows
binaries, or clone the source and compile. Note that compilation requires flex and bison.
- The Linux binary is an 32-bit application. If you are
running a 64-bit Linux implementation that does not already have the
necessary 32-bit libraries installed, please see this
- Looking for SATPLAN-2004/2006? Then go to the SATPLAN home page instead
To get started, try:
Blackbox has many options. For help, run Blackbox with no
options. Blackbox can print the the Boolean formula (in cnf
or literal form), the mapping from literals to propositions, the model
found, and the plan. For example, the following prints
the formula generated by the problem blocks.facts.easy in cnf format:
blackbox -o domain.pddl -f prob004-log-a.pddl
blackbox -o blocks.ops -f blocks.facts.easy -printcnf -printexit
The best solver to use is Chaff.
Version 45 and newer use Chaff by default. For earlier versions,
specify it on the command line:
blackbox -o domain.pddl -f prob004-log-a.pddl -solver chaff
the PDDL input language
Problem domains and problem instances are specifed using the STRIPS
subset of the Planning Domain Definition
Language (PDDL). Blackbox differs from the offical language in the following ways:
- Blackbox assumes that all parameters to an operator must be
bound to different objects. Therefore, inequality preconditions
are not needed (and are ignored if present). Strict equality
conditions are unnecessary (simply use the same variable).
- All of the effects of an action must appear negated in the
precondition of the action. Blackbox won't complain, but the output
will be unpredictable.
- (:requirements) may be :strips, :equality, and/or :typing.
- 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. For example:
lincolncenter - LOCATION jfk - (either AIRPORT LOCATION))
- (:constants) and negated preconditions are not supported.
- Input is case-insensitive.
All (:objects) must be declared in the problem instance. This include
numbers used as arguments to operators.
The domain names must match in the operator and problem instance
controlling the SAT encoding
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
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
64 = include duplicate axioms generated by buggy versions 2.0 and
128 = include axioms that chain from action to action, bypassing facts
(included in Version 3.4)
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 overall design and implementation of blackbox, including the
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
generating and solving SAT representations of planning problems
in STRIPS-like notation.
The front-end of blackbox is a modified version of the code of the graphplan
Blum and Merrick Furst.
- The SAT solver chaff was created by by Sharad Malik
<email@example.com> and colleagues at Princeton
Henry Kautz and Bart Selman (1999).
SAT-based and Graph-based Planning.Proc. IJCAI-99.
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.
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.