xenial (1) anldp.1.gz

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

SEE ALSO

       formed(1), mace2(1), otter(1).
       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).

                                                November  5, 2006                                       ANLDP(1)