Software and Datasets
SatX10: Please visit x10-lang.org/satx10 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 Conﬂicts 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 SAT-07 paper on the practical usefulness of much shorter XORs than the worst case theoretical analysis would suggest, Short XORs for Model Counting: From Theory to Practice: SAT07-suite.tgz (32 KB)
- 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