This is the command anldp that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
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