Instances

The instances for the paper are provided as a tar archive of files that have been individually compressed with xz.

wget https://research.ics.aalto.fi/software/asp/bench/Boosting2019.tar
tar xf Boosting2019.tar

Programs

The program clasp is on github here. The version 3.3.3 is here.

  • Downloading a prebuilt binary of clasp 3.3.3 for linux.

    wget https://github.com/potassco/clingo/releases/download/v5.2.2/clingo-5.2.2-linux-x86_64.tar.gz
tar xf clingo-5.2.2-linux-x86_64.tar.gz
cp clingo-5.2.2-linux-x86_64/clasp .

The program pbtranslate is on github here. It is written in the programming language Crystal. As of this writing, the use of Crystal implies that pbtranslate may only work on Linux and MacOS.

The following are two alternative ways to obtain a binary of pbtranslate.

  • Downloading a prebuilt binary of pbtranslate 0.2.0 for linux.

    wget https://github.com/jbomanson/pbtranslate/releases/download/0.2.0/pbtranslate
chmod +x pbtranslate

    • NOTE: To be precise, In the paper, an earlier version was used corresponding to commit 196bee8 (2018-04-04) and it was compiled with an earlier version of Crystal. The changes since then only aim at making pbtranslate and its specs compile with Crystal 0.27.2, and therefore should not make a difference in the results.

  • Downloading and compiling pbtranslate 0.2.0 from source. This requires crystal to be installed. Version 0.27.2 of crystal should work.

    git clone https://github.com/jbomanson/pbtranslate
cd pbtranslate
git checkout 0.2.0
crystal build --release main.cr -o pbtranslate

In either case, the version reported by ./pbtranslate version should match PBTranslate 0.2.0 [08f4bc8] (2019-02-12).

Note
 Use of crystal build --release would in general be preferrable, but presently it does not work correctly when compiling pbtranslate.

Systems

The systems in the paper correspond to the following pipelines. In the paper, only the CPU times for the last solving stage were recorded.

\(\text{usc}\)

clasp --opt-strategy=usc,1
\(\text{clasp}/L_{0}\)

clasp
\(L_{4}\)

pbtranslate --type o --crop-depth 4 | clasp
\(L_{8}\)

pbtranslate --type o --crop-depth 8 | clasp
\(L_{8}W_{\text{--}}\)

pbtranslate --type o --crop-depth 8 --weight-step 1000000 --weight-last false | clasp
\(L_{16}\)

pbtranslate --type o --crop-depth 16 | clasp
\(L_{32}\)

pbtranslate --type o --crop-depth 32 | clasp
\(\text{F}/L_{\infty}/W_{1}\)

pbtranslate --type o | clasp
\(W_{4}\)

pbtranslate --type o --weight-step 4 | clasp
\(W_{8}\)

pbtranslate --type o --weight-step 8 | clasp
\(W_{16}\)

pbtranslate --type o --weight-step 16 | clasp
\(W_{32}\)

pbtranslate --type o --weight-step 32 | clasp
\(W_{\\infty}\)

pbtranslate --type o --weight-step 1000000 | clasp
\(W_{\text{--}}\)

pbtranslate --type o --weight-step 1000000 --weight-last false | clasp