EnglishFrenchSpanish

Ad


OnWorks favicon

anldp - Online in the Cloud

Run anldp in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

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


Free Servers & Workstations

Download Windows & Linux apps

Linux commands

Ad