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

## AUTHOR

**anldp**ws written by William McCune <[email protected]>

This manual page was written by Peter Collingbourne <[email protected]>, for the Debian project (but may be used by others).