NAME
anldp - implementation of Davis-Putnam propositional satisfiability
procedure
SYNOPSIS
anldp [options] < input-file > output-file
DESCRIPTION
This manual page documents briefly the anldp command.
anldp is an implementation of a Davis-Putnam procedure for the
propositional satisfiability problem. anldp exposes the procedure used
by mace2(1) to determine satisfiability. anldp can also take
statements in first-order logic with equality and a domain size n then
search for models of size n. The first-order model-searching code
transforms the statements into set of propositional clauses such that
the first-order statements have a model of size n if and only if the
propositional clauses are satisfiable. The propositional set is then
given to the Davis-Putnam code; any propositional models that are found
can be translated to models of the first-order statements. The first-
order model-searching program accepts statements only in a flattened
relational clause form without function symbols.
OPTIONS
-s Perform subsumption. (Subsumption is always performed during
unit preprocessing.)
-p Print models as they are found.
-m n Stop when the nth model is found.
-t n Stop after n seconds.
-k n Allocate at most n kbytes for storage of clauses.
-x n Quasigroup experiment n.
-B file
Backup assignments to a file.
-b n Backup assignments every n seconds.
-R file
Restore assignments from a file. The file typically contains
just the last line of a backup file. Other input, in particular
the clauses, must be given exactly as in the original search.
-n n This option is used for first-order model searches. The
parameter n specifies the domain size, and its presence tells
the program to read first-order flattened relational input
clauses instead of propositional clauses.
SEE ALSO
formed(1), mace2(1), otter(1).
Full documentation for anldp is found in
/usr/share/doc/mace2/anldp.{html,ps.gz}.
AUTHOR
anldp ws written by William McCune <otter@mcs.anl.gov>
This manual page was written by Peter Collingbourne
<pcc03@doc.ic.ac.uk>, for the Debian project (but may be used by
others).
November 5, 2006