HordeSat and HordeQBF - Massively Parallel SAT/QBF Solvers

HordeQBF

The paper "HordeQBF: A Modular and Massively Parallel QBF Solver" is submitted (being reviewed) to the 2016 SAT Conference.

Source codes and benchmarks:

• HordeQBF solver source codes: HordeQBF-src.zip [2.8MB] (includes modified source codes of MiniSat and DepQBF 5.0)
• 2014 QBF Gallery benchmarks available at the the QBF Gallery homepage

Experiment logs and evaluation scripts:

The following experimental logs and scripts were used to produce the data presented in the paper.

• DepQBF log files DepQBF-logs.zip [185KB]
• HordeQBF log files HordeQBF-logs.zip [13MB]
• Bash scripts and formated data used to produce the tables and plots of the paper paperdata.zip [119KB]

HordeSAT

The paper "HordeSat: A Massively Parallel Portfolio SAT Solver" was published and presented at the 2015 SAT Conference in Austing, Texas.

Paper and Presentation

• Full paper: horde.pdf
• SAT'15 presentation slides: slides.pdf

Source codes and benchmarks:

• HordeSat solver source codes: hordesat.zip [0.1MB] (includes modified source codes of MiniSat)
• Random benchmarks used in the experiments: random.zip [3.3MB]
• Sat Competition 2014 Application benchmarks link: sc14-app.tar [1.7GB]
• Sat Competition 2011 benchmarks link: SAT11-Competition-SelectedBenchmarks.tar [1.6GB]

Experiment logs and evaluation scripts:

The following experimental logs and scripts were used to produce the data presented in the paper.

• HordeSat on Random 3SAT logs logs-random.zip [8.9MB]
• HordeSat + (p)lingeling on SAT'11 Application Benchmarks app11logs.zip [49.9MB]
• HordeSat + (p)lingeling on SAT'14 Application Benchmarks app14logs.zip [73.9MB]
• Bash scripts used to produce the tables and plots of the paper hordescripts.zip [4KB]