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.
a SAT technology planning system:
blackbox = satplan + graphplan
- Download and run the pre-compiled Linux, Mac OS X, or Windows binaries.
- The source code does not currently compile properly under Linux. Use the precompiled Linux binary (version 43) instead. The current source code has not been tested under Windows.
- Looking for SATPLAN-2004/2006? Then go to the SATPLAN home page instead
To get started,
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). The easiest way to learn the language is to explore the example instances and read:
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:
- 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 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
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)
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 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.
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 <firstname.lastname@example.org> and colleagues at Princeton University.
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 (1999).
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.
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.
notes of the Workshop on Planning as Combinatorial Search, held in conjunction
with AIPS-98, Pittsburgh, PA, 1998.
McDermott and the AIPS-98 Planning Competition Committee. PDDL
- The Planning Domain Definition Language, Draft 1.6, June 1998.