Man Linux: Main Page and Category List

anldp - implementation of Davis-Putnam propositional satisfiability procedure

anldp[options] <input-file>output-file

This manual page documents briefly theanldpcommand.anldpis an implementation of a Davis-Putnam procedure for the propositional satisfiability problem.anldpexposes the procedure used bymace2(1) to determine satisfiability.anldpcan also take statements in first-order logic with equality and a domain sizenthen search for models of sizen. The first-order model-searching code transforms the statements into set of propositional clauses such that the first-order statements have a model of sizenif 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.

-sPerform subsumption. (Subsumption is always performed during unit preprocessing.)-pPrint models as they are found.-mnStop when thenth model is found.-tnStop afternseconds.-knAllocate at mostnkbytes for storage of clauses.-xnQuasigroup experimentn.-BfileBackup assignments to a file.-bnBackup assignments everynseconds.-RfileRestore 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.-nnThis option is used for first-order model searches. The parameternspecifies the domain size, and its presence tells the program to read first-order flattened relational input clauses instead of propositional clauses.

formed(1),mace2(1),otter(1). Full documentation foranldpis found in/usr/share/doc/mace2/anldp.{html,ps.gz}.

anldpws 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