Retrospective Analysis: Refinements of Local Search for Satisfiability Testing
Joachim Walser
Committee: James Crawford
Masters Thesis(Dec 1969)
Keywords:

Local Search routines typically depend on parameters that control the search, such as how long to search before restarting. Optimizing these parameters improves performance and is important for a fair comparison of differing approaches. However, careful optimization is computationally expensive and has been undoable for larger problem sizes.

Here, a probabilistic method, retrospective parameter optimization, is presented. Retrospective analysis allows certain parameters to be tuned using previously collected runtime-data. The method is applied to optimizing mean performance of WSAT on Random 3SAT and scheduling problems by tuning the Max-Flips parameter. Evidence is provided that the optimal value of Max-Flips scales quadratically for Random 3SAT. Further, we show that parallelizing WSAT leads to almost linear speedup on Random 3SAT for a moderate number of processors.

Finally, retrospective analysis is used to test refinements of WSAT, including an implicit propagation mechanism which improves performance on Sadeh's scheduling problems by exploiting their structure.