Proceedings · 2005 · 30 citations · 13 references
Cluster ComputingEngineeringLinear SpeedupComputer ArchitectureParallel ImplementationComputational ComplexityDistributed ExecutionSupercomputer ArchitectureParallel SoftwareSat SolvingSystems EngineeringParallel ComputingSatisfiabilityEssential Optimization TechniquesMassively-parallel ComputingParallel Problem SolvingComputer EngineeringComputer ScienceParallel Sat SolverAutomated ReasoningParallel ProcessingFormal MethodsParallel Programming
In this paper we describe PaMira, a powerful distributed SAT solver. PaMira is based on the highly optimized, sequential SAT engine Mira, incorporating all essential optimization techniques modern algorithms utilize to maximize performance. For the distributed execution an efficient work stealing method has been implemented. PaMira also employs the exchange of conflict clauses between the processes to guide the search more efficiently. We provide experimental results showing linear speedup on a multiprocessor environment with four AMD Opteron processors
13
A machine program for theorem-proving
Martin Davis, George Logemann, Donald Loveland · Communications of the ACM · 1962 · 3.1K citations · Full text
Matthew W. Moskewicz, Conor Madigan, Ying Zhao et al. · 2001 · 2.9K citations
Mathematical Programming, Artificial Intelligence, Constraint Solving +14
Symbolic model checking using SAT procedures instead of BDDs
Armin Biere, Alessandro Cimatti, E. M. Clarke et al. · 1999 · 688 citations
Theory Of Computing, Article Symbolic Model, Engineering +15
GRASP-A new search algorithm for satisfiability
J.P. Marques Silva, Karem A. Sakallah · 2002 · 365 citations