.TH ANLDP 1 "November  5, 2006"
.SH NAME
anldp \- implementation of Davis-Putnam propositional satisfiability procedure
.SH SYNOPSIS
.B anldp
.RI [ options ]
<
.I input-file
>
.I output-file
.SH DESCRIPTION
This manual page documents briefly the
.B anldp
command.
.PP
\fBanldp\fP is an implementation of a Davis-Putnam procedure for the propositional satisfiability problem.  \fBanldp\fP exposes the procedure used by
.BR mace2 (1)
to determine satisfiability.  \fBanldp\fP can also take statements in first-order logic with equality and a domain size \fIn\fP then search for models of size \fIn\fP. 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 \fIn\fP 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.
.SH OPTIONS
.TP
.B \-s
Perform subsumption. (Subsumption is always performed during unit preprocessing.) 
.TP
.B \-p
Print models as they are found. 
.TP
.B \-m \fIn
Stop when the \fIn\fPth model is found. 
.TP
.B \-t \fIn
Stop after \fIn\fP seconds. 
.TP
.B \-k \fIn
Allocate at most \fIn\fP kbytes for storage of clauses. 
.TP
.B \-x \fIn
Quasigroup experiment \fIn\fP.
.TP
.B \-B \fIfile
Backup assignments to a file. 
.TP
.B \-b \fIn
Backup assignments every \fIn\fP seconds. 
.TP
.B \-R \fIfile
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. 
.TP
.B \-n \fIn
This option is used for first-order model searches. The parameter \fIn\fP specifies the domain size, and its presence tells the program to read first-order flattened relational input clauses instead of propositional clauses.
.SH SEE ALSO
.BR formed (1),
.BR mace2 (1),
.BR otter (1).
.br
Full documentation for \fBanldp\fP is found in \fI/usr/share/doc/mace2/anldp.{html,ps.gz}\fP.
.SH AUTHOR
\fBanldp\fP ws written by William McCune <otter@mcs.anl.gov>
.PP
This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
for the Debian project (but may be used by others).