ANLDP(1) General Commands Manual ANLDP(1)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)
Check Out this Related Man Page
MINISAT(1) General Commands Manual MINISAT(1)NAME
minisat - fast and lightweight SAT solver
SYNOPSIS
minisat [options] input-file result-output-file
minisat takes as input a plain or gzipped DIMACS formatted file. The satisfiability of this input problem is indicated both via standard
output and the return value.
DESCRIPTION
This manual page documents briefly the minisat command. MiniSat is a minimalistic, open-source SAT solver, developed to help researchers
and developers alike to get started on SAT. Winning all the industrial categories of the SAT 2005 competition, MiniSat is a good starting
point both for future research in SAT, and for applications using SAT.
Despite the NP completeness of the satisfiability problem of Boolean formulas (SAT), SAT solvers are often able to decide this problem in a
reasonable time frame. As all other NP complete problems are reducible to SAT, the solvers have become a general purpose tool for this
class of problems.
OPTIONS --help, --help-verb Show (verbose) summary of options.
-pre, -no-pre
Enable (default) or disable preprocessing.
-verb {0,1,2}
Set the verbosity of informational output (set to 0 for silent, defaults to 1)
-cpu-lim <unsigned>
Set a limit on CPU time (seconds, defaults to 2147483647).
-mem-lim <unsigned>
Set a limit on memory usage (MB, defaults to 2147483647).
-dimacs <output-file>
Print (possibly preprocessed) input problem in DIMACS format and stop.
-luby, -no-luby
Enable (default) or disable the Luby restart sequence.
-rnd-init, -no-rnd-init
Randomize the initial activity values (defaults to off).
-gc-frac <double>
The fraction of wasted memory allowed before a garbage collection is triggered (non-negative, defaults to 0.2).
-rinc <double>
-var-decay <double>
Variable activity decay factor (0 <= value <= 1, defaults to 0.95).
-cla-decay <double>
Clause activity decay factor (0 <= value <= 1, defaults to 0.999).
-rnd-freq <double>
The frequency with which the decision heuristic tries to choose a random variable (0 <= value <= 1, defaults to 0).
-rnd-seed <double>
Random seed for random variable selection (non-negative, defaults to 9.16483e+07).
-phase-saving {0,1,2}
Controls the level of phase saving (0=none, 1=limited, 2=full, defaults to 2).
-ccmin-mode {0,1,2}
Controls conflict clause minimization (0=none, 1=basic, 2=deep, defaults to 2)
-rfirst <int>
The base restart interval (positive, defaults to 100).
-rcheck, -no-rcheck
Enable (costly) or disable (default) checking for redundant clauses.
-asymm, -no-asymm
Shrink clauses by asymmetric branching (disabled by default).
-elim, -no-elim
Perform variable elimination (enabled by default).
-simp-gc-frac <double>
The fraction of wasted memory allowed before a garbage collection is triggered during simplification (non-negative, defaults to
0.5).
-sub-lim <int>
Do not check if subsumption against a clause larger than this value (-1 <= value, defaults to 1000). -1 means no limit.
-cl-lim <int>
Variables are not eliminated if they produce a resolvent with a length above this limit (-1 <= value, defaults to 20). -1 means no
limit.
-grow <int>
Number of additional clauses that may be introduced when eliminating a variable. Defaults to 0.
EXIT CODES
0 if parsing the command line options fails, usage information is requested, or output of the input problem in DIMACS format succeeds. 1
if interrupted by SIGINT or if an input file cannot be read, 3 if parsing the input fails, 10 if found satisfiable, and 20 if found unsat-
isfiable.
AUTHOR
minisat was written by Niklas Een, Niklas Sorensson
This manual page was written by Michael Tautschnig <mt@debian.org>, for the Debian project (but may be used by others).
September 3, 2011 MINISAT(1)