BORG-SAT-10.04.30

STATUS

This version is a qualification-round preliminary release. If you are studying this code, we strongly recommend that you contact us to obtain a recent source tree. This version is unpolished, in-progress, and contains numerous chunks of obsolete and/or unfinished code.

CONTACT

Bryan Silverthorn [email protected]

COMPILATION

From the src directory, run make. Note that src/Makefile is only a thin wrapper around the richer, cmake-based build system which the src/dep/cargo/run_cmake script will populate under src/dep/cargo/build. The build process requires recent versions of at least:

• gcc
• boost
• cmake
• GSL
• Python
• numpy

This package may include some or all of these dependencies installed under ext/prefix. The solver scripts appropriately set the relevant environment variables.

USAGE

The script "solver" is an entry point to various modules. To solve a SAT instance, use:

./solver utexas.tools.portfolio.solve -v -m ext/dcm_model.pickle --seed <RANDOMSEED> <path/to/instance>

For additional usage information on this portfolio solver, use:

./solver utexas.tools.portfolio.solve --help

To calculate the machine performance calibration score, do:

./solver utexas.tools.calibrate -c ext/calibration.json

SUBSOLVERS

This portfolio solver would not be possible without the immense amount of work done by many other people to create the subsolvers it employs. This release includes:

• CirCUs (Hyojung Han, HoonSang Jin, Hyondeuk Kim, and Fabio Somenzi)
• clasp (Martin Gebser, Benjamin Kaufmann, and Torsten Schaub)
• glucose (Gilles Audemard and Laurent Simon)
• gnovelty+2 (Duc Nghia Pham and Charles Gretton)
• LySATi (Youssef Hamadi, Said Jabbour, and Lakhdar Sais)
• minisat_09z (Markus Iser)
• minisat_cumr_p (Kazuya Masuda and Tomio Kamada)
• MXC (David R. Bregman)
• precosat (Armin Biere)
• rsat (Knot Pipatsrisawat and Adnan Darwiche)
• SApperloT (Stephan Kottler)

LICENSE

This software package is provided under the free non-copyleft "MIT" license. The complete legal notice can be found in the included ext/LICENSE file.