Ubcsat.hpp File Reference

Documentation on how to build and use Ubcsat. More...

Go to the source code of this file.

Detailed Description

Documentation on how to build and use Ubcsat.

Installing and using Ubcsat

On the purpose of Ubcsat

Ubcsat is a collection of procedures for configuring local search SAT solvers.

  • We have tweaked it somewhat to get it closer to a library.
  • We corrected the source code so that it runs also on 64 bit machines.
  • And we made it now flushing it's output.
  • Yet we are using 1.0.0, since we got it working on 64-bit machines. The successor of 1.1.0 should finally work on 64-bit machines, and then we'll update.
  • We also provide a convenience wrapper.

What the installation yields

Via oklib ubcsat we obtain the installation directory /home/csoliver/OKplatform/ExternalSources/Installations/SAT/Ubcsat/1-2-0-beta-17 which contains the following subdirectories:

  • bin contains the executable ubscat, a solver platform which can execute the main local-search algorithms. A link to this program is planted in the public bin-directory (which is /home/csoliver/OKplatform/bin).
  • lib contains the link-libraries which are linked together in the above ubcsat executable, and which are here made available for linking. Compiled with the macro ALTERNATEMAIN, so that no main function is created.
  • The above executable program as well as the link-libraries are compiled using the corrected sources from /home/csoliver/OKplatform/OKsystem/OKlib/Satisfiability/Algorithms/LocalSearch/Ubcsat/corrected.
  • The original sources are copied to the src sub-directory (converted to Unix/Linux line-endings).

Current state of installation

We consider here only the executable:

  • Recommended version = 1-2-0-beta-17
  • ready: MAYBE
    • location = /home/csoliver/OKplatform/ExternalSources/Installations/SAT/Ubcsat/1-2-0-beta-17/bin/ubcsat-1-2-0-beta-17
    • version =


Using the ubcsat-executable:

  • A link is provided in the public bin-directory (/home/csoliver/OKplatform/bin).
  • Using ubcsat -h will show the list of options.
    1. Most useful seems to start with e.g.,
      ubcsat -alg rsaps -runs 100 -cutoff 1000 -i file
      where for the parameter "-alg" one has to chose one of the available algorithms (here "rsaps").
    2. In this way one gets a feeling for the quality of the algorithm, and how cutoff needs to be adapted to the problem at hand.
    3. Additionally the usage of the parameter -noimprove value is of interest, which aborts a run after value-many steps without improvement of the current minimum number of falsified clauses.
  • ubcsat -ha shows the list of available algorithms. Typically one needs to try them all out.

We provide a convenience-wrapper ubcsat-okl (also in the public bin-directory):

  • This calls ubcsat with the parameters -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] -runs 10 -cutoff 100000 -rflush, followed by the parameters given to ubcsat-okl.
  • So we leave out the banner etc., for each run additionally output the seed-value (so that the run can be repeated), and especially provide more statistics about the best assignments found.
  • The wrapper can be used as ubcsat itself, for example
    ubcsat-okl -alg samd -runs 100 -cutoff 10000 -noimprove 1000 -i file

To use Ubcsat-components from inside the OKlibrary:

  • In the ".link_libraries"-file the specification
    echo ${ubcsat_link_option_okl} 
    is needed, which enables linking with all functions and variables provided by the ubcsat-library.
  • For the source-libraries add
    to the definition of source_libraries in definitions.mak: This activates the localised version of header files from the Ubcsat-library, and, if not already overwritten by a localised version, the corrected files (while the other files are taken from the original sources).
  • And the main header file for the Ubcsat-library is OKlib/LocalSearch/Ubcsat/local/ubcsat.h.

How to install

Only local installation.

Make targets

ubcsat Builds the source-library, the link-library and the ubcsat-program, using the system-gcc.
cleanubcsat Removes the build-directory.
cleanallubcsat Removes build- and installation-directories.

Definition in file Ubcsat.hpp.