Using borg¶

Fetching SAT solver binaries¶

In this example, we will build a simple portfolio consisting of several solvers from the 2011 SAT competition. Much of the data from these competitions can be accessed at

http://www.satcompetition.org/

including static binaries of the solvers entered into the competition. Let’s download these and unpack them:

$ wget http://www.cril.univ-artois.fr/SAT11/solvers/SAT2011-static-binaries.tar.gz
$ tar zxvf SAT2011-static-binaries.tar.gz

After unpacking, we find the solvers under SAT2011/bin/static and information about how to execute them inside SAT2011/bin/static/CommandLines.txt.

Selecting solvers to use¶

While a portfolio solver can be a useful tool, it still requires significant domain knowledge to select the solvers to include in the portfolio. In this example, we will simply select three of the best-performing solvers from the 2009 SAT competition and the 2010 SAT race:

• cryptominisat (Mate Soos),
• clasp (Martin Gebser, Benjamin Kaufmann, and Torsten Schaub), and
• TNM (Wanxia Wei and Chu Min Li).

This selection follows the lead of the ppfolio tool, a basic parallel portfolio that performed well in the 2011 competition. More information is available in its documentation.

Since ppfolio has helpfully packaged these solvers for the 2011 competition, we can access them inside the SAT2011/bin/static/main/sat11-11-roussel/bin directory. Let’s make a symlink to that directory with

$ ln -s SAT2011/bin/static/main/sat11-11-roussel/bin ppfolio-bin

so that we can access it more easily later.

Constructing a solver suite¶

We will now write a configuration file that allows borg to execute these SAT solvers by name. In borg, a collection of named solvers is referred to as a “suite”.

A suite configuration file is simply a Python module that establishes how to execute each solver. Here is a configuration file for the suite of solvers selected above:

import borg

domain = borg.get_domain("sat")
commands = {
    "cryptominisat": ["{root}/ppfolio-bin/cryptominisat", "--randomize={seed}", "{task}"],
    "clasp": ["{root}/ppfolio-bin/clasp", "--seed={seed}", "{task}"],
    "TNM": ["{root}/ppfolio-bin/TNM", "{task}", "{seed}"],
    }
solvers = borg.make_solvers(borg.domains.sat.solvers.SAT_SolverFactory, __file__, commands)

We will call this file suite_sat_ppfolio.py.

A solver suite is required to provide two top-level variables:

• domain, which must be an instance of a class such as borg.domains.sat.Satisfiability that allows borg to parse instances of the problem domain, compute features on those instances, and determine basic properties of “answers” to instances of the domain; and
• solvers, a dictionary that maps arbitrary solver names (e.g., “minisat”) to instances of a solver factory class, such as borg.domains.sat.solvers.SAT_SolverFactory, that allow borg to initiate solver runs on problem instances and to understand their output.

borg includes support for the output formats of various common solver types. In this case, the class borg.domains.sat.solvers.SAT_SolverFactory supports the typical output format of SAT competition entries.

Gathering training instances¶

In this example, we will collect such data for the ppfolio suite on a small set of instances from the SAT2011 competition. Unfortunately, doing so requires downloading the entire set of instances from the competition:

$ mkdir benchmarks
$ cd benchmarks
$ wget http://www.cril.univ-artois.fr/SAT11/bench/SAT11-Competition-SelectedBenchmarks.tar
$ tar xvf SAT11-Competition-SelectedBenchmarks.tar

The archive contains a huge number of individually compressed instances. For now, we will train our portfolio on a small subset of those instances. The easiest way to create such a subset is simply to symlink or copy the relevant instances into a common location—here, into a new directory named “selected”:

$ mkdir selected
$ cd selected
$ cp ../SAT11/random/large/unif-k3-r4.2-v10000* .
$ cp ../SAT11/application/fuhs/AProVE11/* .
$ bunzip2 \*.bz2

We have now pulled together an arbitrarily selected set of 20 instances to use as our training set.

Executing solvers repeatedly¶

Borg can use an HTCondor or IPython.parallel cluster to execute solvers repeatedly and collect training data. For this experiment, set up a local IPython cluster by running:

$ ipcluster start -n 2

In this invocation, the ipcluster script will launch two engines for parallel processing. The value of the “-n” argument can be bumped up if you have more cores.

The borg run_solvers tool collects run duration data. By default, it uses the local IPython cluster. To invoke it, specify the portfolio configuration above (in this case, “suite_sat_ppfolio.py”), the directory containing the set of benchmarks on which to execute the solver suite (in this case, “benchmarks/selected”), and the run duration cutoff in seconds (in this case, 300 seconds).

$ python -m borg.tools.run_solvers suite_sat_ppfolio.py benchmarks/selected/ 300

File format: subsolver run records¶

Run records are typically stored in CSV files with the suffix .runs.csv. The full suffix can be modified through the “-suffix” flag to run_solvers, among other borg tools.

The following columns are expected in the following order:

solver

Unique name of the solver.

budget

Budget allotted to the run, in CPU seconds.

cost

Computational cost of the run, in CPU seconds.

succeeded

Did the solver succeed on this run?

answer

Base64-encoded gzipped pickled answer returned by the solver on this run, if any.

File format: instance features¶

Instance features are stored in CSV files with the suffix .features.csv. The first column must be cost, the computational cost of feature computation, in CPU seconds. The remaining columns are domain-specific, one per feature.