Man Linux: Main Page and Category List


       anldp  -  implementation  of  Davis-Putnam propositional satisfiability


       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.


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


       formed(1), mace2(1), otter(1).
       Full       documentation      for      anldp      is      found      in


       anldp ws written by William McCune <>

       This   manual    page    was    written    by    Peter    Collingbourne
       <>,  for  the  Debian  project  (but  may  be used by

                               November  5, 2006