anldp(1) 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.

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