Captain Jack Captain Jack :: The SAT Solver

Department of Computer Science, The University of British Columbia and
Institute of Theoretical Computer Science, Ulm University


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


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


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