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)