general.hpp File Reference

General plans regarding monitoring solvers. More...

Go to the source code of this file.

Detailed Description

General plans regarding monitoring solvers.

Handling changing solver output
  • A solver's output can be different depending on the options given to it.
  • For instance, the OKsolver_2002 will output the additional attributes, "splitting directory" and "splitting cases", if one passes in the "-S" option, but not otherwise. This is discussed in "Handling splitting output" in ExperimentSystem/SolverMonitoring/plans/OKsolver.hpp. OK: as discussed there, no such case distinctions should be performed.
  • The question is how extraction scripts, as described in "Extraction tools" below, should handle different outputs from the same solver. OK: use NA-values.
  • The two most natural options are:
    • Extraction scripts take solver arguments: OK: as explained above, this should not be done.
      • Extraction scripts take the solver options as arguments and extract different attributes depending on these arguments.
      • The advantage with this method is that the output of the extraction script never has any missing data.
      • The disadvantage is that the system becomes more complicated, and one must remember what options were passed to the solver.
    • Default values for missing data:
      • Extraction scripts always output a column for all possible data that the solver outputs. When the solver doesn't output certain data, the extraction script outputs a default value.
      • For the default value, we have two choices: use a default value which could be output by the solver (e.g., 0, or whatever is sensible for the attribute in question), or use special NA values (from R).
      • Using "zero" values has the advantage that a table with these values can have statistics calculated, without additional measures taken.
      • Using NA values has the advantage that it is always clear that a value is missing, and it isn't mistaken for "real" data.
      • Obviously the NA-value is the *only* possibility, since the data is statistical data, and we obviously follow the practice of statistics in their own field. And values 0 would just be false in general.
  • In general, it seems best to some form of default values for missing data, avoiding the additional complexity of script arguments.
  • DONE (if the field is not output by the solver, then obviously it gets the NA-value --- never 0; all initialisations must always use NA, and in this way automatically we get NA in case the solver didn't give data) The use of "zero" or NA values should be a matter decided on an attribute by attribute basis.
  • DONE (there should be no such cases) The use of additional options for the extraction scripts should be reserved for special cases, where the additional complexity seems warranted.
Testing solver extraction scripts
  • We need tests to ensure that the extraction scripts collect the statistics correctly.
  • Testing solvers behave as we expect:
    • Solvers change from version to version, and depending on this update, there are three possible scenarios:
      • The solver has changed very little, and works and outputs basically the same thing, and so the extraction scripts and aspects of the library don't need to change.
      • The solver has changed its output format slightly, or some minor aspect of its inner workings, and so we wish to update extraction scripts to reflect this.
      • The solver is very different, and should be considered a different solver entirely, with new extraction scripts.
    • We should provide a method of testing that a solver outputs exactly the format that we expect:
      • What data is output?
      • Is this data as we expect, given our knowledge of the current behaviour of the solver?
      • Is the data still output in the same format?
    • Such a test allows us to then detect small changes in a solver which might break extraction scripts and other tools, but are small enough to go unnoticed; perhaps an attribute we rarely look at changes.
    • This test would also make it easier to write extraction tools for new versions of solvers with large differences, as it acts as a form of documentation of the features and output format we expect of the previous version.
Running experiments
  • Compare "run_ubcsat as shell script" in ControllingLocalSearch/plans/DataCollection.hpp for a similar system; one should create a general naming scheme.
  • Currently we have RunMinisat.
  • Running experiments from a directory by "ExpRunMinisat":
    • Often we have a directory full of instances which we wish to run a solver on in a specific order.
    • The order we wish to run the solver in is usually dependent on a parameter, present in the filename of the instance.
    • However, a better solution, which by itself documents which instances were considered in each order, and which is also simpler, just uses a file with one instance per line.
    • We should provide a mechanism for running the solver on instances given by such a file, and collecting the statistics.
    • We have several possibilities:
      • Manually running the solvers on each instance, and providing a script which collects Statistics from a number of Experiment directories into a single Statistics file.
      • Adding a "--dir" option to RunMinisat etc. which processes a directory of instances, and creates a directory with all of the RunMinisat directories inside it, plus an overall Statistics file.
      • Best is to provide a dedicated script, ExpRunMinisat, which creates, as usual, an experiment directory, copies and documents its arguments, which are typically configuration-files, and then runs the computations.
      • Important that this script can be (just) restarted.
      • One needs to see whether the script itself collects the statistics from the various experiment-directories, or whether that is done by an external tool.
    • DONE (this is a bad hack) In each case we need standard tools to extract parameters from filenames; see also "Extraction tools".
  • Statistics:
    • These scripts should also (at least) collect full data on the true number of variables, clauses and literals present in the instance, adding this data to the Statistics file as the n, c and l columns.
    • Computation as with the OKsolver_2002, that is, tautological clauses and repeated literals are removed, and then c is the number of remaining clauses, l the number of remaining literal occurrences, and n the number of remaining variables.
    • We likely also want to collect more statistics on these instances, for example, min/max/avg clause-length, deficiency and so on.
  • We need scripts like that for all solvers.
Better summary statistics
  • It it important that functions like read_processsplit_minisat (in CubeAndConquer.R) automatically output good summary statistics (since typically only these numbers will be used).
  • Currently we use "summary".
  • We should also use "sd", possibly also "mean" (already provided in summary, but now with a different formatting, better suited for sd).
  • Library "pastecs" offers "stat.desc", which has more on the side of variance.
  • Library "Hmisc" offers "describe", which has more quantiles, and a bit of other data.
  • We need to provide our own summary-functions, tailored for the special situations.
  • For a start, see the approach in CubeAndConquer.R:
    1. The general functions there, once approved, need to move to more general places.
Extraction tools
  • The most fundamental tool for a solver is a script, which takes the solver output from standard input, and puts it into a single line (just data) on standard output, usable for R.
  • First we implement this as an awk script (with documentation of all attributes, in the docus):
    • ExtractGrasp.awk
    • ExtractArgosat.awk
    • ExtractCryptominisat.awk: DONE
    • ExtractPicosat.awk : DONE
    • ExtractMinisat.awk : DONE
    • ExtractOKsolver.awk : DONE
    • ExtractGlucose.awk : DONE
    • ExtractPrecosat236.awk
    • ExtractPrecosat570.awk : DONE
    • ExtractSatz.awk : DONE
    • ExtractMarchpl.awk : DONE
  • We should provide tests for all of these scripts, as discussed in "Testing solver extraction scripts" above.
  • DONE (see ExtractMinisat for the role model) This is without parameters; with parameter "header" (as string) it just prints the header (which is also at the top of the R-output).
    1. How to handle this data-dependency?
    2. Perhaps, at least at the beginning, we just state in comments that the header must be the same as used in the awk-script, but don't provide some mechanism for avoiding the duplication.
    3. The string uses a single space for separation, and no leading or trailing space(-symbols).
    4. The header-string is provided in a data-file, e.g., "Minisat.header". Or one could use a directory "headers", containing e.g. "minisat" etc.
    5. In case something else than "header" is provided to the script, and which can not be interpreted, an error occurs.
    6. Best we have possible parameter-values "header-only" and "data-only" (while without anything both header and data are printed).
  • DONE (actually, we don't need such a script since it is the task of the experiment-processing script to collect all data into statistics-files, at the time when the data is created) And with parameter "dir=Directory" it reads all the files in Directory, and prints to standard output the header followed by the data-lines.
  • DONE (no need anymore, see above) Then an additional column with the filename is added:
    1. No path information, just the basename.
    2. Having the possibility for extracting information from the filename is also needed.
    3. This information can be given as a string which specifies a sed-script (for transforming the R-output).
    4. Parameter "extraction=sed-string".
    5. If "header" is provided to the script, then the user must also provide the header for the additional parameter.
    6. Parameter "extraction_header=string".
  • Then we do not need wrappers. This is better since it avoids possible complications.
  • Remark: with the Ubcsat-wrapper it's different, since there we only need to supply default parameter (which can also be overwritten if needed).
  • For each solver-class we have such a script:
    1. ExtractMinisat (see ExperimentSystem/SolverMonitoring/plans/Minisat2.hpp).
    2. ExtractPicosat (see ExperimentSystem/SolverMonitoring/plans/Picosat.hpp).
    3. ExtractOKsolver (see ExperimentSystem/SolverMonitoring/plans/OKsolver.hpp).
    4. ExtractGlucose (see ExperimentSystem/SolverMonitoring/plans/Glucose.hpp).
    5. ExtractSatz
    6. ExtractMarchpl (not yet implemented)
    7. To be completed
  • Standardised column names:
    1. n : integer, number of variables.
    2. rn : integer, number of variables as reported by the solver.
    3. c : integer, number of clauses.
    4. rc : integer, number of clauses, as reported by the solver.
    5. l : integer, number of literal occurrences.
    6. rl : integer, number of literal occurrences, as reported by the solver.
    7. mcl : integer, maximal clause length.
    8. rmcl : integer, maximal clause length, as reported by the solver.
    9. Such general measures (n, c and l) always refer to the original input (not after preprocessing).
    10. t : double, solution time (in seconds).
    11. sat : in {0,1,2} for UNSAT, SAT, UNKNOWN.
    12. nds : double, number of nodes for look-ahead solvers.
    13. cfs : double, number of conflicts for conflict-driven solvers.
    14. dec : double, number of decisions for conflict-driven solvers.
    15. rts : double, number of restarts.
    16. r1 : double, number of unit-clause propagations.
    17. r2 : double, number of failed-literal reductions.
    18. pls : double, number of pure literals.
    19. ats : double, number of autarkies (not pure literals).
    20. h : integer, height of search-tree for look-ahead solvers.
    21. mem : double, in MB.
    22. ptime : double, parse time (in seconds).
    23. file : string.
    24. bnds : double, number of backtracking-nodes (exactly two successor).
    25. snds : double, number of single-nodes (exactly one successor).
    26. lvs : double, number of leaves (no successor).
    27. r2la : double, number of r_2-look-aheads (for r_2-reductions).
    28. r3 : double, number of r_2-reductions.
    29. r3la : double, number of r_3-look-aheads (for r_3-reductions).
    30. There can be more attributes; the above ones always occur in that order.
    31. DONE (no need to make incomparable data comparable) For handling parameters that aren't produced by certain solvers, for example nds by minisat-2.2.0, there are two options:
      1. Output "NA" for that column.
      2. Don't output an nds column. This has the disadvantage that outputs from different solvers are harder to compare.
      For now the awk scripts (see above) don't output the column.
  • Some solvers do not always output their full statistics. In such cases, appropriate 0-values have to be entered. This is discussed in "Handling changing solver output".
  • DONE (solver-outputs in general are not comparable, only similar families of solvers should be treated similarly) Not all solver outputs are comparable.
    • DONE (different solvers have different interpretations, that's it; if we want additional input statistics, then it can be easily provided for each investigation) Variable numbers:
      • Consider the Dimacs file:
        shell> cat test.cnf
        p cnf 100 1
        100 0
      • OKsolver_2002 returns the true number of variables:
        shell> OKsolver_2002-O3-DNDEBUG test.cnf
        c initial_number_of_variables           1
      • minisat-2.2.0 returns the upper bound on the variable index:
        shell> minisat-2.2.0 test.cnf
        |  Number of variables:           100                                         |
      • DONE (no need) We should output both of these outputs (true number and maximum variable index).
  • With such tools in place, the current R-functions should be transformed to functions for reading and evaluating files created with the tools.
  • We need also a simple system to connect a solver with its extraction tool:
    1. So that in an application, where the solver is run, one can also easily do the extraction.
    2. Perhaps just a helper-shell-script "ExtractInfo", which takes the solver-name as input, and returns the name of the extraction-script.
Add monitoring for all other solvers
  • This is about analysing the "verbose" output.
  • For OKsolver_2002 we have some functions in OKsolver.R.

Definition in file general.hpp.