rkstoreyomi(3) [debian man page]

RKSTOREYOMI(3)						     Library Functions Manual						    RKSTOREYOMI(3)

NAME

       RkStoreYomi - change the reading of the current clause, reconverting the subsequent clauses

SYNOPSIS

       #include <canna/RK.h>
       int RkStoreYomi(cxnum, yomi, maxyomi)
       int cxnum;
       unsigned char *yomi;
       int maxyomi;

DESCRIPTION

       RkStoreYomi  changes the reading of the current clause to a specified reading, reconverting the subsequent clauses.  It changes the reading
       yomi with a length of maxyomi bytes.  The value of maxyomi must be adjusted to character boundaries in the EUC code.

RETURN VALUE

       This function returns the number of clauses after the change.

																    RKSTOREYOMI(3)

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)