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).