SATPLAN USERS GUIDE
				   
		     Henry Kautz and Bart Selman
 			     AT&T Research
			     June 3, 1996

I. Introduction

Satplan is a planning system that works by converting planning
problems into propositional satisfiability, and then solving those
instances using general satisfiability algorithms.  Although the
program is targeted for planning, it can be easily adapted to generate
and solve encodings of other kinds of combinatorial problems.

The system consists of three basic parts:
	"satplan" generates a cnf encoding;
	"solve" tries to find a satisfying truth assignment for the instance;
	"interpret" prints the satisfying truth-assignment in an
		understandable form

For example, suppose the file "bw_orig.ops" contains a set of
operators for the blocks world, and "anomaly.facts" contains a problem
specification for the well-known Sussman anomaly.  Then the follow
series of commands generates a cnf encoding of the anomaly, solves it,
and prints the result:

	satplan -o bw_orig -f anomaly
	solve anomaly -s t
	interpret anomaly

A copy of the interpretation is also saved in the file "anomaly.interp".

The fastest way to get started is to try the examples in the examples/
directory of the distribution.  Below we describe each of the three
programs in detail, and then describe the format of operator and facts
files.

II.  Installation

See the file system/README.install for information on installing the
system.  Note that the instructions for installation include setting
an environmental variable SATPLAN to the directory containing the system.

III.  Satplan

Satplan is invoked as follows:
	satplan -o OPERATORS -f FACTS -t STEPS
where

OPERATORS is a file containing axioms specific to a planning
	domain.  This filename must end with the extension ".ops"
	(which may be omitted on the command line: 
	"-o foo" is the same as "-o foo.ops").
	The OPERATORS file may appear in either the current working
	directory or in $SATPLAN/lib.

FACTS is a file containing the specification (initial and goal state)
	of the particular plannning instance.
	This filename must end with the extension ".facts"
	(which may be omitted on the command line: 
	"-f foo" is the same as "-o foo.facts").
	The FACTS file must appear in the current working directory.

STEPS is an integer, giving the maximum time step in the plan.  Times
	thus range from 0 up to STEPS.  For domains where all actions
	are sequential (e.g. the blocks world), STEPS is the same as
	the number of actions in the solution.  For domains where
	actions can be performed in parallel (e.g. the logistics
	domain), STEPS is the amount of time needed to perform the
	plan assuming maximum parallelization.  If STEPS is not given
	on the command line, then the default value specified in the
	FACTS file is used.

	The size of the encoded problem instance grows rapidly with STEPS,
	so you want to keep it as small as possible.  Whether or not a solution	
	exits to a problem when STEPS is set too large depends upon whether
	the particular domain axioms allow "null" actions to pad out
	the solution.  The logistics.ops axioms in effect allow null actions;
	the bw_orig.ops axioms do not.  (It is not difficult, however, to
	devise versions of the blocks world axioms that do allow null actions.)	

When Satplan runs, it generates two files:
	FACTS.cnf - contains the problem as an propositional
		satisfiability problem.  The format of the file is:
		1. Lines beginning with "c" are comments - must appear first.
		2. A line of the form
			p cnf N M
		   where N is the number of variables and M is the number
		   of clauses.
		3. A series of clauses, one per line, of the form
			N1 N2 N3 ... 0
		   where each number Ni stands for a proposition,
		   negated to mean "NOT", and ending with a 0.

		The comments in the file specify when the wff was generated,
		what axioms were used, and other helpful information.

	FACTS.map - contains the information used by interpret (see below)
		to reconstruct the solution in terms of named literals
		(e.g. "on(A,B,3)") instead of numbered propositions.

Satplan works as follows:

1.  OPERATORS.ops and FACTS.facts are combined with header files kept
in SATPLAN/lib to creat a C program.  This program is compiled and
executed.

2.  Execution of this program generates a formula using ground,
instantiated literals.

3.  The literal version of the formula is turned into one made up of
numbered propositions.

4.  The formula is simplified by unit propagation, subsumption, and
deletion of unit clauses.

IV.  Solve

The program "solve" provides a uniform interface to different
satisfiability testing programs, currently walksat, tableau, and ntab.
It's basic use is:
	solve  FILE.cnf -solver K {-out SOLNFILE } { solver specific options }
where
	FILE.cnf is created by satplan; the .cnf extension may be
		omitted ("FILE" is the same as "FILE.cnf").
		If the -solver option is given but FILE.cnf is not,
		then the wff is read from stdin.
	
	K is one of t (for tableau), n (for ntab), or w (for walksat).

	SOLNFILE is the name of file where the solution is saved,
		along with comments that record the exact parameters
		used by the solver.  If this option is not specified
		but FILE.cnf is, then the solution is saved in FILE.out.

If the -solver option is not given on the command line, then solve
prompts the user for missing options.  Type "solve -help" to see the
full list of options.

When solve runs, it prints tracing information to the screen and saves
the trace, solution, and comments in the file FILE.out (or in the file
specified by the -out option).  FILE.out also contains comments
specifying the date and the exact options used for the solver.  Note
that the actual truth-assignment found is saved in FILE.out, but is
not printed to the screen.

If a solver is specified on the command line but no FILE.cnf is given,
then solve reads from STDIN and writes to the screen; a solution file
is created only if an explicit -out option is included.
The following are exactly equivalent:
	solve -solver t foo.cnf
	solve -solver t -out foo.out < foo.cnf
The following is "almost" equivalent; however, in this case foo.out
does not include the solution itself, nor the header comments that are
used by the "interpret" program discussed below:
	solve -solver t < foo.cnf > foo.out

A note on Walksat:  the Walksat solver is randomized algorithm.  The
default option is for walksat to exit as soon as solution is found.
To gather good timing statistics, however, you may want to solve the
problem instance many times.  To do this, use the "-m" option:
	solve foo.cnf -solver w -tries 100 -m
performs exactly 100 tries (restarts), no matter how many tries (if
any) ends in a solution.  On the other hand,
	solve foo.cnf -solver w -tries 100
performs AT MOST 100 tries, but terminates as soon as a solution is
found.  For more information on options to walksat, type
	solve -solver w -help

V.  Interpret

Interpret takes a solution file in the FILE.out format and pretty
prints it.  Both the FILE.out and the corresponding FILE.map file must
be in the current working directory.  To invoke it simply type
	interpret FILE.out
where the ".out" extension is optional.  IMPORTANT: if .out extension
is omitted, as in
	interpret FILE
then Interpret will try to simply read FILE, and only if it does not
exist, will it look for FILE.out.

The pretty-printed solution is sent to both the screen and to the file
FILE.interp.  If no file is specified on the command line, then the
interpretation is sent only to STDOUT.  Thus
	interpret < foo.out > foo.interp	
	interpret foo.out
are equivalent.

Interpret determines the name of the map file to use from the comments
embedded in the .out file, rather than from the name of the .out-type file.
The name of the .interp file IS based on name of the .out-type file.
Thus, the following sequence:
	satplan -o bw_orig -f anomaly
	solve -solver t anomaly -out tableau_soln
	solve -solver w anomaly -out walksat_soln
	interpret tableau_soln
	interpret walksat_soln
correctly creates the following files:
	tableau_soln.interp
	walksat_soln.interp
This feature makes it easier to keep around multiple versions of
solution files to a single problem.

VI.  The OPERATOR and FACTS file

Now we come to the trickiest part of the Satplan system, the OPERATOR
and FACTS file formats.  If you examine some example files, you will
see that both are fragments of code in the C programming language.
By compiling an operator and facts file together with
	$SATPLAN/instantiate.c
	$SATPLAN/instantiate.h
Satplan creates an program whose execution instantiates a set of axiom
schemas over a specified domain.

The two "instantiate" files contain general type definitions, macros,
and utility functions.  The FACTS file typically contains some global
data structures, used to specify the initial and goal states.  Most of
the work is done in the OPERATORS file.  This file contains a "main"
function that calls a series of functions, the execution of each of
which generates a set of clauses.

Consider the file bw_orig.ops.  It begins with external declarations
for the variable "goal", which is the maximum time step; the "init" and
"final" STATES; and two DOMAINS of objects, one called "block" and the
other called "fixed".  All these variables are given values in a
particular .facts file (e.g., anomaly.facts).

    #include "instantiate.h"
    
    extern int goal;
    extern STATE init;
    extern STATE final;
    extern DOMAIN block;
    extern DOMAIN fixed;
    
The "main" function (re)sets the value of the goal variable (if a -t
option is specified when satplan is invoked), and calls functions,
defined in that same file, to generate general axioms for moving
blocks, and about the predicate "on":

    int main(int argc, char *argv[])
    {
        if (argc > 1){
    	if (sscanf(argv[1], " %d", &goal)!=1)
    	  error("Must supply number of goal step on command line");
        }
    
        blocks_axioms();
        on_axioms();
    
Finally, the main function calls the function complete_state (also
defined in this file) that generates clauses describing the initial
and final states, using the values for the corresponding STATE
variables defined in whatever .facts file is linked in.

        complete_state(init, 0);
        complete_state(final, goal);
        end_wff();
        return 0;
    }
    
Look now at anomaly.facts.  Here we see domain entities are simply
represented by strings.  A DOMAIN is a null-terminated array of
strings.  The default value for the goal is timestep 3:

    DOMAIN block = { "A", "B", "C", "TABLE", NULL };
    DOMAIN fixed = { "TABLE", NULL };
    int goal = 3;

STATES are again simply null-terminated arrays of strings.  The exact
interpretation of a STATE depends on the particular functions called
in the .ops file (here, the function "complete_state" is called).

    STATE init = { 
        "A", "B",
        "B", "TABLE",
        "C", "TABLE",
        NULL
      };
    
For these blocks axioms, a STATE is assumed to be an exhaustive list
of pairs, where the first element of each pair on "on" the second
element.  In other domains (such as logistics.ops), STATES have a
different interpretation.  (See specific comments on the domains
below.)

Finally, let us turn to the functions that actually generate the
axioms.  Consider the function blocks_axioms.  It begins as follows:

    void blocks_axioms()
    {
        int i;
    
        for (i=0; i<goal; i++) {
    
This part means that the following clauses will be instantiated over
times i that range from 0 to (goal-1).  Next come a series of macros
in the form of axiom schemas.  Let us consider the first one:

	All(x, block, !member(x, fixed),
	    All(z, block, !eql(x,z),
		Disj(
		     Not( L2( "object", x, i));
		     Not( L2( "destination", z, i));
		     L3( "on", x, z, i + 1))));

This schema begins by declaring a variable x that ranges over elements
of domain "block" that are NOT also elements of the domain "fixed".
Then it declares a variable z that ranges over blocks that are
different from x.  (Inequality here just means that the strings that
represent the domain elements differ.)  The macro Disj indicates the
beginning of a clause.  Each clause generated by this schema contains
3 literals.  The first literal is generated by:
		     Not( L2( "object", x, i));
The Not means that the literal is negated.  "L2" indicates a predicate
schema that takes two arguments.  The name of the predicate is
"object".  The first argument is x, and the second is the time step i.
All the arguments EXCEPT the last in a predicate schema must
instantiate to strings (i.e., be elements of some DOMAIN).  The last
argument is always a time index, which is of type int.

This is the most common form of a clause schema:  a series of nested
universal quantifications, enclosing a Disj.  Sometimes you want to
get the effect of existential quantification.  For example, there is
an axiom that asserts that at every time, there exists some block for
which the predicate "object" holds.  Existential quantification is
done by nesting an All quantifier INSIDE the scope of the Disj
(instead of outside).  Thus, we write:

	Disj( All( x, block, ! member( x, fixed),
		 L2("object",  x, i)));

When this macro is executed for a particular value of i, it creates
one long clause, each of whose elements is a literal with predicate
"object".  So, if the non-fixed blocks are A, B, and C, then the
clauses generated by this schema (where i ranges from 0 to 3) are:
	
	( object(A,0) object(B,0) object(C,0) )
	( object(A,1) object(B,1) object(C,1) )
	( object(A,2) object(B,2) object(C,2) )
	( object(A,3) object(B,3) object(C,3) )
	

The following summarizes the macros and functions available to the
user writing an operators file, where

	"stmt" means something that expands to a
		(possibly complex) C statement (which could
		include a sequence of ;-separated statements).
	"cond" means something that expands to a C expression;	
	"var" is a variable;
	"domain" is the name of a domain, i.e. a pointer to a null
		terminated array of strings.

All( var, domain, cond, stmt )
-- Variable var iterates over the domain; for bindings which satisfy
cond, the stmt is instantiated.  The variable is
of type char *.   IMPORTANT: the expression "cond" is evaluated at
INSTATIATION time (when the clauses are generated); it does not
actually become part of the wff itself.  It is also important to 
understand that all the variables that appear in cond must be bound in
a larger scope; free variables cannot appear.  If cond is always true,
then use the value 1.

Disj( stmt )
-- Generate a clause by executing stmt.  Note that stmt is typically a
;-separated list of statements, one for each disjunct of the clause.

L3( pred, arg1, arg2, t )
L2( pred, arg1, t )
L1( pred, t )
L0( pred )
-- Instantiate the given n-ary predicate.  The LAST term in L3, L2, and
L1 is an int rather than a string varible.

Not( literal )
-- Argument should be one of the predicate macros above.

int member( str, dom )
-- True if string str is in the domain dom.

eql( str1, str2 )
-- True if strings are equal.

In addition to these basic functions, there are also functions that
make it easier to deal with "static" relations, that is ones that do
not vary over time.  An element being a member of a DOMAIN is one kind
of (unary) static relation.  There are also functions to handle 2 and
3 place static relations.  Note that static relations do not appear as
predicates instantiated in the wff itself; instead, they typically
appear in cond-expressions to control the expansion of the schema.

For example, in the logistics, there is a static relation LOC_CITY
that relates an object (postoffice, airport, or truck) to the the city
to it's city.  (Trucks do not move between cities in this domain.)
So, in the file examples/logistics.facts we see:

    STATIC_RELATION LOC_CITY = {
     "pgh-po", "pgh",
     "pgh-airport", "pgh",
     "bos-po", "bos",
     "bos-airport", "bos",
     "la-po", "la",
     "la-airport", "la",
     "bos-truck", "bos",
     "pgh-truck", "pgh",
     "la-truck", "la",
     NULL };

LOC_CITY is a 2 place relation.  (There is no explicit declaration of
the arity of static relation.)  The tests:

int reln2( rel, arg1, arg2 )
int reln3( rel, arg1, arg2, arg3 )

test if a 2 or 3 place static relation (respectively) hold.

The proper use of static relations in the conditions of All schemas
can greatly reduce the size of the instantiated wff.  But keep in mind
the restriction that free variables cannot appear in a cond.  For
example, the following schema (alone) is not a legal way to talk about
trucks an airports in the same city:

	All(x, TRUCK, 1,
       		All(y, AIRPORT, reln2(LOC_CITY, x, z) && reln2(LOC_CITY, y, z),
			Disj( ... )))

Instead, you need to explicity bind the variable z:

	All(z, CITY, 1,
		All(x, TRUCK, reln2(LOC_CITY, x, z),
       			All(y, AIRPORT, reln2(LOC_CITY, y, z),
				Disj( ... ))))

VII.  The Blocks World Operators

This section briefly discusses some of the non-obvious features of the
blocks world axioms, in bw_orig.ops.

The domains are:
	block - all objects (both movable and stationary).
	fixed - the subset of (stationary) blocks that act as "tables".

The predicates are:
	on(x,y,i) - x is on y at time i.
	clear(x,i) - if x is not fixed, then nothing is on x at time i.
		if x is fixed, then this predicate is meaningless.

A block is moved at every time step (except the last).  Instead of a
single "move" predicate, there are 3 predicates:
	object(x,i) - x is the block moved at time i
	source(y,i) - y is the thing x was sitting on at time i
	destination(z,i) - z is the thing x is sitting on at time i+1.

The semantics are:
	- only non-fixed blocks can be "on" something.
	- at most one block can be on a non-fixed block.
	- any number of blocks can be on fixed block.
	- non-fixed blocks are always on something.
	- exactly one block is moved at each time step.

VIII.  The Logistics Operators

This section briefly discusses some of the non-obvious features of the
logistics axioms, in logistics.ops.

The domains are:
	OBJECT - packages that need to be moved around.
	TRUCK - can carry packages within a CITY (cannot move between
		cities); is always at some LOCATION in its home CITY.
	LOCATION - a place within a city; includes AIRPORTS and post offices.
	AIRPORT - there is one per city; is a subclass of LOCATION.
	CITY - a city; contains TRUCKS and LOCATIONS.

The static relation
	LOC_CITY - relates a TRUCK or LOCATION to its home CITY.
The function
	same_city(arg1, arg2)
returns true if the two things specified have the same home CITY.

The predicates are "at" and "in":
	at - an OBJECT, TRUCK, or AIRPLANE can be at a location.
	in - an OBJECT can be in a TRUCK or AIRPLANE.

Any number of non-interfering actions can occur at each time step.
There are no explicit action predicates; instead, the axioms state
what kind of changes in the "at" and "in" predicate are possible:

	- a TRUCK can go from being at one LOCATION to another in the
		same city.

	- an AIRPLANE can go from being at one AIRPORT to another.

	- an OBJECT can go from being at a LOCATION to being in a
		TRUCK or AIRPLANE that is at that same location
		(loading).    The truck or airplane cannot move
		while it is loading.

	- an OBJECT can go from being in a TRUCK or AIRPLANE 
		to being at the LOCATION where that vehicle is.
		(unloading).  The truck or airplane cannot move
		while it is unloading.


IX.  Additional Scripts

In addition to the functions described above, the distribution (as of
June 96) includes a script "preprocess", invoked as any of:

	preprocess FILE
	preprocess FILE.lit
	preprocess FILE.cnf

This is a general script for preprocessing and simplifying wffs, and
creates the proper headers in the resulting files for use by solve and
interpret.  The FILE can contain either a wff in .cnf format, or one
in "literal formal": that is, lines of the form:
	( literal1 literal2 ... )
where a literal is either
	atom
or 
	NOT atom
and an "atom" is an arbitrary string not containing whitespace.

Preprocess generates the files
	FILE.s.cnf
	FILE.s.map
where the ".s" indicates the file has been simplified.  If simplify
solves the formula, it also generates
	FILE.s.out
Then, to solve and interpret the results perform
	solve {options} FILE.s
	interpret FILE.s
(note that the .s must be included).