Alef® - Cluster SAT Solver
Alef is a distributed, multi-processor SAT solver designed to leverage
cluster computing resources connected via MPI. Alef provides scalable
performance to customers with an interest in solving the sort of hard
structured SAT instances that occur in scientific, planning, and
verification applications.
The Alef solver works by spawning cooperating searches spanning a variety
of tactics and uses an innovative algorithmic approach that allows
cooperating instances to share useful learned information. Unlike
competing parallel approaches that attempt to strictly partition the search
space, Alef uses randomness and learned information about infeasible
solutions to naturally drive cooperating searches to distinct parts of the
search space. The result is an approach to cooperative parallelism where
communication can be throttled in such a way that it never overwhelms the
search routines themselves. Through communication throttling, Alef can
function as an ensemble solver with no coordination, but openning
communication leads to an additional performance benefit as cooperating
searches exchange intermediate results.
The Alef solver incorporates the best and most novel published ideas from
the academic SAT community and extends them with proprietary tactics that
provide an additional performance benefit. In a single node configuration,
Alef is competitive with the best open solvers and provides an increasing
performance advantage as additional resources are supplied. On a 32-node
Xeon cluster, a 5-7x performance improvement is typical for non-trivial
structured SAT instances. This improvement has led to Alef finding
solutions to published benchmarks that competing open sequential solvers
have not previously been able to tractably resolve.
Alef is built on the MPI message passing standard and has been tested to
work with both the MPICH2 and OpenMPI implementations. Alef supports the
standard DIMACS CNF input format and is intended as a drop-in replacement
for existing sequential SAT solvers.
Alef® Key Benefits
- Fast: Alef integrates the best, most recent innovations from academic
solvers with advanced Reservoir Labs technology that allows cooperating
searches to efficiently share information. Performance scales with
cluster size, but experiments on a 32-node cluster suggest a 5-7x
performance improvement is typical for industrial benchmarks.
- Configurable: Whether working on a single desktop or a large
heterogeneous cluster, Alef makes efficient use of the resources
available.
- Tunable: Alef is capable of adapting its rate of information sharing to
the available bandwidth. So whether running on a fast-interconnect
supercomputer or a distributed cluster, Alef won't bog down from
coordination overhead.
- Compatible: Alef accepts problems in the standard DIMACS CNF format. No
special problem preconditioning is required to take advantage of Alef on
cluster resources.
- East-to-use: Alef messaging is built on the standard MPI protocol and
works properly with both the MPICH2 and OpenMPI implementations.
Version 2.3 now available for all UNIX platforms. For more information about Alef, including licensing terms, please contact us.
|
