anldp - Online in the Cloud

PROGRAM:

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.

Use anldp online using onworks.net services