Alef parallel SAT solver for HPC hardware

ABSTRACT

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications, including formal verification of both hardware and software, mathematics, and planning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a parallel SAT solver, Alef, to take advantage of HPC hardware.The Alef parallel SAT solver utilizes algorithms and heuristics that improve its performance over existing approaches. We are developing the solver to run well on commercially available HPC hardware. Our analysis shows that our algorithms combined with the low message latency of supercomputers are likely to produce a significant performance improvement over existing solvers in terms of speed and maximum problem size. Our poster will describe the algorithms we are using, illustrate our approach to problem partitioning, and present our performance analysis to date.

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.6 Optimization

Additional Classification:
  G. Mathematics of Computing
  G.1 NUMERICAL ANALYSIS
      G.1.0 General
  G.4 MATHEMATICAL SOFTWARE
      Subjects: Parallel and vector implementations

General Terms:
Algorithms, Design