Provided by:

mace2_3.3f-1.1_amd64 **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 __n__th 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 ANLDP(1)