Implementation of davis-putnam propositional satisfiability procedure
anldp [options] < input-file > output-file
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.
Perform subsumption. (Subsumption is always performed during unit preprocessing.)
Print models as they are found.
Stop when the nth model is found.
Stop after n seconds.
Allocate at most n kbytes for storage of clauses.
Quasigroup experiment n.
Backup assignments to a file.
Backup assignments every n seconds.
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.
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.