Software and Datasets

SatX10: Please visit to download SatX10, our recent Scalable Plug&Play Parallel SAT Solver design and evaluation framework, built using the X10 parallel programming and execution language.

Due to copyright restrictions, this download contains only a patch file and for one base SAT solver. If you would like to try SatX10 with multiple solvers, or are interested in adding a new solver, please let us know!

Data for experiments reported in my publications:

  • Data for the CPAIOR-2013 paper, Stronger Inference Through Implied Literals from Conflicts and Knapsack Covers: CPAIOR2013-impliedLitsMIP.txt
  • CNF formulas used in the NIPS-2011 paper on FocusedFlatSat for Density of States computation, Accelerated Adaptive Markov Chain for Partition Function Computation: NIPS2011-suite.tgz (100 KB)
  • CNF formulas used in the ANOR-2011 paper on BPCount and MiniCount for model counting, Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting: ANOR2011-suite.tgz (5.3 MB)
  • CNF formulas used in the IJCAI-07 paper on SampleCount for model counting, From Sampling to Model Counting: IJCAI07-suite.tgz (3.5 MB)
  • CNF formulas used in the NIPS-06 paper on XOR based sampling, Near-Uniform Sampling of Combinatorial Spaces Using XOR Constraints: NIPS06-suite.tgz (12 KB)
  • CNF formulas used in the AAAI06 paper on XOR based model counting, Model Counting: A New Strategy for Obtaining Good Bounds: AAAI06-suite-v2.tgz (1 MB), please see note about PHP formulas
  • CNF formulas used in the AAAI05 paper on symmetry breaking, SymChaff: A Structure-Aware Satisfiability Solver: AAAI05-suite.tgz (links to Cornell)