AAAI Publications, Twenty-First International Joint Conference on Artificial Intelligence

Font Size: 
Integrating Systematic and Local Search Paradigms: A New Strategy for MaxSAT
Lukas Kroc, Ashish Sabharwal, Carla P. Gomes, Bart Selman

Last modified: 2009-06-25


Systematic search and local search paradigms for
combinatorial problems are generally believed to
have complementary strengths. Nevertheless, attempts
to combine the power of the two paradigms
have had limited success, due in part to the expensive
information communication overhead involved.
We propose a hybrid strategy based on
shared memory, ideally suited for multi-core processor
architectures. This method enables continuous
information exchange between two solvers
without slowing down either of the two. Such a hybrid
search strategy is surprisingly effective, leading
to substantially better quality solutions to many
challenging Maximum Satisfiability (MaxSAT) instances
than what the current best exact or heuristic
methods yield, and it often achieves this within seconds.
This hybrid approach is naturally best suited
to MaxSAT instances for which proving unsatisfiability
is already hard; otherwise the method falls
back to pure local search.


Satisfiability; Constraint Optimization; Search; SAT and CSP: Solvers and Tools; MAX-SAT

Full Text: PDF