general.hpp File Reference

General documentation on the original OKsolver. More...

Go to the source code of this file.

---

Detailed Description

General documentation on the original OKsolver.

The OKsolver from 2002

This first version of the OKsolver is made accessible here. Since it has a rather canonical "semantics", it can serve as a kind of standard implementation of

• a look-ahead solver
• who employes full failed-literal-reduction ("r_2")
• and full unit-clause-propagation ("r_1") look-ahead.

The heuristics is given by (weigthed) counting of new clauses, and here naturally basic autarky reduction (generalising pure-literal-elimination) is utilised.

Specification

Procedural specifications at the Lisp/Maxima level are given in ComputerAlgebra/Satisfiability/Lisp/Backtracking/OKsolver2002.mac.

Macro options

The most important macro options (that is, compile time options):

• If NBAUMRES is defined, then tree resolution pruning ("intelligent backtracking") is turned off, while otherwise (the default) it is turned on (that is, BAUMRES gets defined).
  • If NLITTAB is defined, then the more space efficient (but less time time efficient) special datastructure is not used.
  • Otherwise (the default) it is used (that is, LITTAB gets defined).
• If ASSIGNMENT is defined, then if a satisfying assignment is found, it is output, while otherwise only the satisfiability status is returned. (Internally, ASSIGNMENT is translated yet into BELEGUNG.)
• If OUTPUTTREEDATAXML is defined, then the search tree is output into a file, using a simple XML structure and adorning each node with some statistics.
• NOT IMPLEMENTED YET If ALLSAT is defined, then all satisfying assignments are found. Currently combination with BAUMRES or ASSIGNMENT is not possible (and thus yet we just count all satisfying assignments.
  • NSAT_BITS specifies the number of bits for the unsigned int value of the number of satisfying assignments.
  • The default is 64, and it can be set to any value supported by your platform.
  • Overflows are not detected, and the number of satisfying assignments is thus only correct modulo 2^NSAT_BITS (however whether the value is 0 or not is correctly reported).

Precompiled programs

The optimised version of a program has the optimisation options in the name. The following programs are created (in both versions, unoptimised and optimised), as usual in /home/csoliver/SAT-Algorithmen/OKplatform/system_directories/bin:

1. OKsolver_2002 (the default version; a link is also provided in the public bin-directory /home/csoliver/SAT-Algorithmen/OKplatform/bin)
2. OKsolver_2002_NTP (no tree pruning)
3. OKsolver_2002_NLT (tree pruning needs more space, but is faster)
4. OKsolver_2002_osa (outputs satisfying assignments)
5. OKsolver_2002_NTP_osa
6. OKsolver_2002_NLT_osa

Basic usage

• Call the OKsolver with one parameter, the filename containing the CNF in DIMACS format.
• The OKsolver accepts also arbitrary non-empty sequences of digits and letters for variable-names, with the exception that in DIMACS format a first character must not be "0", "p" or "c".
• By default satisfying assignments are not output, but this can be turned on, and also all output can be printed into a file.
• A monitoring level of the search tree can be established, such that finished nodes at this level are reported, and predicated running times are computed.

Command-line options

The solver reads the arguments in order, processes each and exits.

• Without any argument just a short instruction is printed.
• Option --help creates a short help message.
• --version prints version information.
• --author prints information about the author.
• --info shows how to interpret the (standard) output.
• --specification prints a solver specification in XML.
• --language=x switches the output-language; supported values are x=0 for German and x=1 for English (the default).
• --timeout=n for a time-out in n seconds (wall-clock), where n=0 means no time-out.
• --standard=x switches the input-format; supported values are
  1. x=1 for DIMACS (the default; as always, "extended", allowing names for variables).
  2. x=2 uses "%" for beginning a comment (anywhere), "(" for opening a clause, ")" for closing a clause, and literals are separated by a comma.
  3. x=3 as x=2 but (arbitrary) space symbols separate literals.
  4. x=4 as x=3, but no clause-begin, and line-end finishes a clause.
  The restrictions for variable-names (not beginning with "0,c,p") only hold for DIMACS (x=1). DIMACS does not accept an empty clause, while the other formats do.
• Toggles (switching between "ON" and "OFF"):
  • -F for printing the results also to files (default is OFF).
  • -M for monitoring the level d of the backtracking tree (default is OFF), where d=6 by default (watching 2^6 = 64 nodes).

    d can be set using-Dd, for example -D10 for watching 2^10 = 1024 nodes at depth 10. Range 0 <= d <= 30.

    Once a node at level d is completed, its number is printed out, followed by the number of leaves below it, the total running-time until now, and the anticipated running time for the remaining nodes at this level, using the current average running time for the monitored nodes (always in seconds).

    If file-output is activated, then the monitoring output is echoed to file "FullInputFileName.mo".

• To be completed.

Signals

Given the process identity id, a signal called "SIGNAL" is sent to the process via kill -s SIGNAL id.

• Sending the signal SIGUSR1 to the OKsolver causes the printout of the current statistics.
• Sending the signal SIGINT to the OKsolver aborts the computation after printing the statistics. This signal is send to a program when pressing CTRL C on the command line.

Output

• Explanation of the output for the (default) DIMACS output:
  1. The number of variables is always (before and after reduction) the number of variables actually occurring in the clause-set.
  2. "reduction" refers to elimination of tautological clauses, repeated literal occurrences and unit-clause-propagation.
  3. reduced_maximal_clause_length: how much the maximal clause-length was decreased by the reduction.
  4. reduced_number_of_variables: How many variables where eliminated by the reduction.
  5. reduced_number_of_clauses: How many clauses where eliminated by the reduction.
  6. reduced_number_of_literal_occurrences: How many literal occurrences where eliminated by the reduction.
  7. initial_number_of_2-clauses: Number of 2-clauses after reduction.

Definition in file general.hpp.