Ubcsat-okl.hpp File Reference

Plans on the wrapper for Ubcsat. More...

Go to the source code of this file.

Detailed Description

Plans on the wrapper for Ubcsat.

More readable large numbers
  • See "Contact the developers of Ubcsat" in Satisfiability/Algorithms/LocalSearch/Ubcsat/plans/general.hpp.
  • Especially for the cutoff value it would be good if number representations like "100*10^6" (or "55*11^7") could be used.
  • It's awkward to count the zeros.
  • So ubcsat-okl needs to parse the parameters, and translates numbers like that into their decimal representation.
  • In order to avoid misinterpretations, perhaps we only consider a "-cutoff" parameter.
  • A little awk-script could do the job:
    1. Its input is the whole parameter line.
    2. Running through the parameters one searches for "-cutoff".
    3. The parameter after "-cutoff" is first devided by "*" into (a,x), and if x is present, x is divided into (b,c) by "^", and then a * b^c (where a, b, c are natural numbers) is computed.
    4. Returned is the whole parameter line, with the cutoff-value replaced.
Better output
  • DONE (completed plans for improved output) See ExperimentSystem/ControllingLocalSearch/plans/DataCollection.hpp for plans on extending resp. using the output-functionality.
  • The idea is that ubcsat-okl creates some form of complete output, which is directly readable by R (into a dataframe, without further processing).
  • By appropriate formatting one also might make it better readable for the human reader.
  • DONE (we don't do this; ubcsat version 2.0 will be rather different, so we do only simple things for now) Since we reformat the output, the wrapper should likely reformat every single output line individually (as it comes, so that one can read into R also partial results (from the intermediate file)).
  • DONE (don't need the algorithm-names here) The following seems reasonable as a "ubcsat-okl" script:
    # Work out algorithm argument
    ALG_ARG_P=1; for arg_p in `seq 1 $#`; do 
      if [[ ${!arg_p} == "-alg" ]] ; then ALG_ARG_P=`expr $arg_p + 1`; fi;
    ALG=`printf '%34s' ${!ALG_ARG_P}`
    echo "       sat  min     osteps     msteps       seed                                alg"
    ubcsat -rclean -r out stdout run,found,best,beststep,steps,seed -r stats stdout numclauses,numvars,numlits,fps,beststep[mean],steps[mean+max],percentsolve,best[min+max+mean+median] $* | sed -e "s/^\\(\\( \\+[0-9]\\+\\)\\{6\\} *\\)$/\\1${ALG}/"
    This appends the algorithm as a column to the data, line by line.
  • Various output parameters:
    1. Should this script also take into account that the user may want to specify different output parameters, and then provide different headers for when this is the case?
    2. No, we just provide the current, "default" version, and an additional full version (which provides all data).
    3. The name of the additional script shall be "fubcsat_okl".
  • We also need the DIMACS output codes (10 for satisfying assignment found, 0 for unknown):
    1. If it can be done easily, then we modify the ubcsat-source.
    2. Otherwise we wait for version 2.0.
  • Another point is how to handle statistics as they are only printed at the end (and this in a form incompatible with the R-format).
    1. It should be easy to patch the ubcsat-code, so that these statistics are printed out with an additional "# " in front (so they are commented-out for R).
    2. Also run_ubcsat then needs to be adapted.
  • DONE A problem appending columns line by line to ubcsat output is that ubcsat version 1.0.0 doesn't flush data, and so one would have to wait until ubcsat has finished before viewing results. See "Ubcsat does not flush the output-buffer" below for how to repair this.

Definition in file Ubcsat-okl.hpp.