---
name: "anldp"
section: "1"
platform: "linux"
package: "mace2"
version: "3.3f-1.1"
release: "Debian 8 (Jessie)"
platforms: ["linux"]
url: "https://new.carta.tech/anldp"
---

# anldp(1)

implementation of Davis-Putnam propositional satisfiability procedure

## 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)](/mace2/1.md) 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)](/formed/1.md), [**mace2**(1)](/mace2/1.md), [**otter**(1)](/otter/1.md).\
 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).