• 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 askubuntu page.
• Looking for SATPLAN-2004/2006?  Then go to the SATPLAN home page instead 

To get started, try:

cd Examples/logistics-strips
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

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:
          (:objects  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 files.

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)

• 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 system of Avrim Blum and Merrick Furst.
• The SAT solver chaff was created by by Sharad Malik <sharad@ee.princeton.edu> and colleagues at Princeton University.