Sciweavers

SAT
2004
Springer

Local Search for Very Large SAT Problems

13 years 9 months ago
Local Search for Very Large SAT Problems
The Walksat local search algorithm has previously been extended to handle quantification over variables. This greatly reduces model sizes, but in order to guide greedy moves the algorithm still maintains a set of violated clauses. For very large problems, or at the start of a search, this can cause memory problems. We design a new local search algorithm that does not maintain this set and is therefore applicable to larger SAT problems. We show that this algorithm is nevertheless greedy in a probabilistic sense, and that it has good performance on some SAT problems. We also describe a prototype lifted version of the algorithm, and show that advanced constraint programming techniques pay off when searching for violated clauses.
Steven David Prestwich, Colin Quirke
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SAT
Authors Steven David Prestwich, Colin Quirke
Comments (0)