General documentation on the original OKsolver. More...

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 employs full failed-literal-reduction ("r_2")
and full unit-clause-propagation ("r_1") look-ahead.

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

Specification

See the report "Investigating the behaviour of a SAT solver on random formulas" available at http://cs.swan.ac.uk/~csoliver/papers.html#OKsolverReport2002 .
Procedural specifications at the Lisp/Maxima level are given in ComputerAlgebra/Satisfiability/Lisp/Backtracking/OKsolver2002.mac.
A general theoretical underpinning is given in the SAT Handbook article " Fundaments of Branching Heuristics" available at http://cs.swan.ac.uk/~csoliver/papers.html#Handbook2009Fundaments .

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.) Compare switch "-O" below.

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.

The output is stored in the file "filename.xml", where filename is the (full) name of the input file.

The embedded DTD is

<!DOCTYPE t [
  <!ELEMENT t (t?, t?)>
  <!ATTLIST t
    l NMTOKEN #REQUIRED>
]>

The attribute-value for "l" is the number of r_2-reductions at the node.

An example (created by "oklib_load_all(); output_sdk_EasterMonster();" in Maxima):

> OKplatform/system_directories/bin/OKsolver_2002_OUTPUTXML-O3-DNDEBUG S_EasterMonster.cnf
s SATISFIABLE
c sat_status                            1
c initial_maximal_clause_length         9
c initial_number_of_variables           729
c initial_number_of_clauses             10551
c initial_number_of_literal_occurrences 23349
c number_of_initial_unit-eliminations   490
c reddiff_maximal_clause_length         3
c reddiff_number_of_variables           490
c reddiff_number_of_clauses             8984
c reddiff_number_of_literal_occurrences 19739
c number_of_2-clauses_after_reduction   1343
c running_time(sec)                     0.0
c number_of_nodes                       9
c number_of_single_nodes                0
c number_of_quasi_single_nodes          0
c number_of_2-reductions                100
c number_of_pure_literals               0
c number_of_autarkies                   0
c number_of_missed_single_nodes         0
c max_tree_depth                        3
c proportion_searched                   8.750000e-01
c proportion_single                     0.000000e+00
c total_proportion                      0.875
c number_of_table_enlargements          0
c number_of_1-autarkies                 0
c number_of_new_2-clauses               0
c maximal_number_of_added_2-clauses     0
c file_name                             S_EasterMonster.cnf

> cat S_EasterMonster.cnf.xml
<?xml version="1.0" standalone="yes" ?>
<!DOCTYPE t [
  <!ELEMENT t (t?, t?)>
  <!ATTLIST t
    l NMTOKEN #REQUIRED>
]>

<t l="0"><t l="7"><t l="9"></t>
<t l="25"></t>
</t>
<t l="9"><t l="12"></t>
<t l="4"><t l="10"></t>
<t l="24"></t>
</t>
</t>
</t>

The solution was found in the right-most branch.

This tree as a labelled (binary) Maxima-tree is (using lists of values as labels (here of length 1)):

T :
  [ [0],
  [ [7],
    [[9]],
    [[25]]
  ],
  [ [9],
    [[12]],
    [ [4],
      [[10]],
      [[24]]
    ]
  ]
]$

This Maxima representation is computed by "Xml2Maxima":

> Xml2Maxima S_EasterMonster.cnf
> cat S_EasterMonster.cnf.mac
T_oklib :
[[0],[[7],[[9]],[[25]]],[[9],[[12]],[[4],[[10]],[[24]]]]];

Draw with "draw_lrt(T_oklib);" (in Maxima).

If SYSTIME is defined, then instead of the standard time measurement from the C-library the Unix/Linux time measurement from sys/times.h is used.
- This enables to measure longer times on 32-bit machines, and thus this is the default on 32-bit machines.
- While otherwise the standard time measurement is sufficient, and so SYSTIME is not defined here.
- To define SYSTIME, pass the option
```
CFLAGS="-DSYSTIME"
     
```
  to the oklib call.
- If on the other hand on a 32-bit machine this system time should not be used, then pass the option
```
CFLAGS="-UMACHINE_BITS_OKL"
     
```
  to the oklib call (this makes temporary the machine a non-32-bit machine).
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/OKplatform/system_directories/bin:

OKsolver_2002 (the default version; a link is also provided in the public bin-directory /home/csoliver/OKplatform/bin)
OKsolver_2002_NTP (no tree pruning; link provided in /home/csoliver/OKplatform/bin)
OKsolver_2002_NLT (tree pruning needs more space, but is faster)
OKsolver_2002_osa (outputs satisfying assignments)
OKsolver_2002_NTP_osa
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 given, 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.
Output formats:
1. -DO for printing the output in Dimacs format (this is the default).
  - Here the possible results "SATISFIABLE, UNSATISFIABLE, UNKNOWN" are in the first line of the output, which starts with "s ".
  - Followed by comment-lines (which start with "c ") with statistics.
  - Finally, if output of satisfying assignments is activated (see switch "-O" below), then in one line, starting with "v ", the list of literals set to true is output (separated by spaces), concluded by " 0" (as with clauses).
2. -XO for printing the output in XML format.
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 (called a "monitoring node"), its number is printed out, followed by
    1. the number of nodes created after the last monitoring node has been completed,
    2. the current average of the number of nodes created per monitoring node,
    3. the predicted total number of nodes,
    4. the (processor) time it took to process the current monitoring node,
    5. the current average time it took to process a monitoring node,
    6. the predicted remaining running time (which is just the current average time multiplied with the number of remaining monitoring nodes),
    7. the number of nodes realised (after the last monitoring node) to have only one child due to tree-pruning,
    8. the number of autarkies (after the last monitoring node),
    9. finally the total tree depth.
  - If file-output is activated (via "-F"):
    1. The monitoring output is echoed to file "FullInputFileName.mo".
    2. The output to the file is more machine-readable, and the predictions are left out since they are easily computable.
    3. As an additional output one has the average number of 2-reductions ("failed literals") since the last monitoring node.
    4. Also output of branching literals for the monitoring levels up to 2 levels before the monitoring level is activated (only to the file).
    5. This output consists of three numbers, first the level, then the name of the variable, and then the first truth value to be visited by the solver.
    6. However, in order for this to work, currently also output of satisfying partial assignments (if found) is to be activated (via "-O").
- -P for only performing preprocessing (cleaning of input and unit-clause-propagation). Some applications:
  - By
```
> OKsolver_2002-O3-DNDEBUG -P Filename | awk '$2 == "initial_number_of_variables" {print $3}'
       
```
    the (precise) number of (occurring) variables is computed (without any reduction).
  - And by
```
> OKsolver_2002-O3-DNDEBUG -P Filename | awk '$2 == "initial_number_of_clauses" {print $3}'
       
```
    the (precise) number of clauses is computed (without any reduction).
- -R for the special DIMACS return values (default is ON in case of DIMACS output, and OFF otherwise).
- -O for output of a satisfying assignment (if found; default is OFF, however if macro ASSIGNMENT is set (see above) then the default is ON).
- -SF for saving the partial assignments for the splitting instances created by "-S" (see below) in a (single) file; default is OFF, storing the partial assignments each in its own file.
-S=directory resp. -S=file:
1. Whether the directory- or the file-form is active depends on "-SF" (see above).
2. The directory must already exist and must be writable.
3. The file will be created if needed.
4. Uses the depth-parameter "-D=d" as above for monitoring.
5. Stores the partial assignments leading to the (reduced) nodes with at least d assignments (decisions and enforced) of the splitting tree, from left to right.
6. The main usage is for splitting a hard problem into (at most) 2^d many subproblems; see below for helper scripts.
7. The partial assignments yielding the sub-problems are stored either in files 1, ... in directory, or line by line in the specified file.
8. Additionally the decisions variables for each splitting are output:
  1. Always in a (single) file, either in file decisions in the directory, or in the file filename_decisions.
  2. The format is one line per splitting, first the number of decisions, and then the 0-based indices of the decisions in the corresponding partial assignment.
9. The DIMACS format for partial assignments is used (see above).
10. Via the switch "-SD" the interpretation of d is changed:
  1. The criterion for aborting the development of the splitting tree is changed.
  2. After the switch, the depth of the node is considered; this is equal to the number of decision variables on the path to the node.
  3. The default is to consider the size n of the partial assignment leading to the node; so also inferred assignments and autarky assignments are taken into account.
  4. The default is the "n-interpretation", and the switch changes it to the "depth-interpretation".
  5. As usual with such switches, another application switches it back to the default value, and so on.
11. A special case is "-D0": Here now in file directory/1 (or in the single line of the output-file) one finds the partial assignment for the fully reduced input --- not just cleaning-up and unit-clause-propagation (as "-P" above), but also r_2-reduction and the associated autarky-reduction.
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. And also the number of clauses is the precise count (before and after reduction).
3. "Reduction" refers to
  1. elimination of tautological clauses and repeated literal occurrences
  2. unit-clause-propagation.
4. So initial_number_of_variables is the precise number of variables in the input (taking also tautological clauses into account), while initial_number_of_clauses is the precise number of clauses in the input (again, taking also tautological clauses into account).
5. The "reddiff"-information specifies the difference achieved by the reduction:
  1. reddiff_maximal_clause_length: how much the maximal clause-length was decreased by the reduction.
  2. reddiff_number_of_variables: how many variables were eliminated by the reduction.
  3. reddiff_number_of_clauses: how many clauses were eliminated by the reduction.
  4. reddiff_number_of_literal_occurrences: how many literal occurrences were eliminated by the reduction.
6. The "proportion"-information refers to the proportion of the 2^n (total) assignments which has been covered by the splitting-tree:
  1. proportion_searched refers to the proportion without the contribution of tree-pruning.
  2. proportion_single refers to the proportion due to the contribution of tree-pruning alone.
  3. total_proportion finally is the sum (equal to 1 for unsatisfiable inputs).
7. In case the "-S" option is used, we have the "splitting"-information:
  1. splitting_directory is the directory, or file if "-SF" is used, containing the splitting data.
  2. splitting_cases is the number of sub-instances generated by the splitting.
The return values for the DIMACS output:
1. 10 for "SAT"
2. 20 for "UNSAT"
3. 0 for "unknown".
For non-DIMACS output the return value is 0 for all cases of proper exit.

Combination with pre-processors

Combination with the Minisat2 pre-processor:
1. This combination seems often quite successful, and is provided by the wrapper script OKsolver_2002-m2pp.
2. Same parameters as the OKsolver, while creating a temporary file containing the preprocessed file.
3. Two additional outputs are provided before calling the OKsolver: Statistics on the original input, and the output of the Minisat2 preprocessor.

Splitting into sub-problems

For hard problems we have the script SplittingViaOKsolver.
This is a script for calling the OKsolver with the option "-S"; see above for some details of this option.
As explained above, this uses the depth-option "-D=d" as above, however not for monitoring, but for outputting the sub-instances of the splitting at depth d.
The parameters of SplittingViaOKsolver are passed over to the OKsolver, adding the parameter "-S=dir" with appropriate value for dir, the splitting-directory.
The script creates the splitting-directory, calls the OKsolver, and stores all data related to this computation in files in this directory.
See the documentation of SplittingViaOKsolver.
To process the created splitting-directory, use ProcessSplitViaOKsolver (see the documentation).
To extract the spliting-information as an iCNF-file, use ExtractiCNF (see the documentation).
If for splitting only the decision-assignments shall be used, use ExtractDecisionsiCNF (see the documentation).
For processing an iCNF-file, we have ProcessiCNF (see the documentation). Note that compared to ProcessSplitViaOKsolver this has less information available.
In order to extract the decision-assignments into a DNF (which yields an unsatisfiable tree-hitting clause-set) we have the application CollectingDecisions (see the documentation).

Definition in file general.hpp.