Captain Jack :: The SAT Solver Department of Computer Science, The University of British Columbia and Institute of Theoretical Computer Science, Ulm University

Introduction

Captain Jack is a highly parametric stochastic local search algorithm for solving SAT.

Publications

A preprint of the final Captain Jack paper is available [here].
An detailed experimental appendix (still in a rough draft) is available upon request.

Software

Captain Jack is included in ubcsat (since version 1.2-beta12).

You should use the most recent version.

(the build used to generate the data in the SAT 2011 paper is ubcsat 1.2-beta12 available [here])

Instance Sets

Each of the data sets are split into a training and a test set:

Instance-Specific Parameter Files

The final parameter settings found by ParamILS and used to generate the results in the SAT11 paper are [here].

to use these files with ubcsat, you can simply use:

ubcsat -alg jack -fp parameterfile

(we have also provided all of the preliminary parameter settings used in the experiments [here]; the final parameter settings are the phase3 results)

ParamILS Configuration Files

The configuration files used to configure Captain Jack with ParamILS are available [here].

(we have also provided all of the configuration files used in each phase of the experiments [here])

Citation / BibTeX entry

@inproceedings {sat11-jack,
  author =        "Dave A. D. Tompkins and Adrian Balint and Holger H. Hoos",
  title =         "{C}aptain {J}ack: New Variable Selection Heuristics in Local Search for {SAT}",
  booktitle =     "Proceedings of the Fourteenth International Conference on Theory and Applications of Satisfiability Testing ({SAT 2011})",
  pages =         "302--316",  
  year =          "2011",
  series =        "Lecture Notes in Computer Science",
  volume =        "6695",
  editor =        "Karem Sakallah and Laurent Simon",
  publisher =     "Springer Berlin / Heidelberg"
}

Authors & Additional Links

• Dave Tompkins
• Adrian Balint
• Holger Hoos