OKlibrary
0.2.1.6
|
General documentation on the original OKsolver. More...
Go to the source code of this file.
General documentation on the original OKsolver.
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
The heuristics is given by (weighted) counting of new clauses, and here naturally basic autarky reduction (generalising pure-literal-elimination) is utilised.
The most important macro options (that is, compile time options):
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). NLITTAB
is defined, then the more space efficient (but less time time efficient) special datastructure is not used. LITTAB
gets defined). 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. OUTPUTTREEDATAXML
is defined, then the search tree is output into a file, using a simple XML structure and adorning each node with some statistics. <!DOCTYPE t [ <!ELEMENT t (t?, t?)> <!ATTLIST t l NMTOKEN #REQUIRED> ]>
> 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>
T : [ [0], [ [7], [[9]], [[25]] ], [ [9], [[12]], [ [4], [[10]], [[24]] ] ] ]$
> Xml2Maxima S_EasterMonster.cnf > cat S_EasterMonster.cnf.mac T_oklib : [[0],[[7],[[9]],[[25]]],[[9],[[12]],[[4],[[10]],[[24]]]]];
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. SYSTIME
is not defined here. CFLAGS="-DSYSTIME"
CFLAGS="-UMACHINE_BITS_OKL"
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. NSAT_BITS
(however whether the value is 0 or not is correctly reported). 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
The solver reads the arguments in order, processes each and exits.
--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 -DO
for printing the output in Dimacs format (this is the default). -XO
for printing the output in XML format. -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). -Dd
, for example -D10
for watching 2^10 = 1024 nodes at depth 10. Range 0 <= d <= 30. -P
for only performing preprocessing (cleaning of input and unit-clause-propagation). Some applications: > OKsolver_2002-O3-DNDEBUG -P Filename | awk '$2 == "initial_number_of_variables" {print $3}'
> OKsolver_2002-O3-DNDEBUG -P Filename | awk '$2 == "initial_number_of_clauses" {print $3}'
-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
: directory
, or line by line in the specified file. decisions
in the directory, or in the file filename_decisions
. 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. Given the process identity id
, a signal called "SIGNAL" is sent to the process via kill -s SIGNAL id
.
SIGUSR1
to the OKsolver causes the printout of the current statistics. 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. 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). reddiff_maximal_clause_length
: how much the maximal clause-length was decreased by the reduction. reddiff_number_of_variables
: how many variables were eliminated by the reduction. reddiff_number_of_clauses
: how many clauses were eliminated by the reduction. reddiff_number_of_literal_occurrences
: how many literal occurrences were eliminated by the reduction. proportion_searched
refers to the proportion without the contribution of tree-pruning. proportion_single
refers to the proportion due to the contribution of tree-pruning alone. total_proportion
finally is the sum (equal to 1 for unsatisfiable inputs). splitting_directory
is the directory, or file if "-SF" is used, containing the splitting data. splitting_cases
is the number of sub-instances generated by the splitting. 10
for "SAT" 20
for "UNSAT" 0
for "unknown". 0
for all cases of proper exit. OKsolver_2002-m2pp
. SplittingViaOKsolver
. SplittingViaOKsolver
are passed over to the OKsolver, adding the parameter "-S=dir" with appropriate value for dir, the splitting-directory. SplittingViaOKsolver
. ProcessSplitViaOKsolver
(see the documentation). ExtractiCNF
(see the documentation). ExtractDecisionsiCNF
(see the documentation). ProcessiCNF
(see the documentation). Note that compared to ProcessSplitViaOKsolver
this has less information available. CollectingDecisions
(see the documentation). Definition in file general.hpp.