Transcript Local search characteristics of incomplete SAT procedures

Local search characteristics of
incomplete SAT procedures
Tang Yi
Based on [1]
Local search methods
• Effective engineering methods for finding
satisfying assignments
• Incomplete and cannot prove if the solution
exists
• Systematic understanding remains elusive
• Analysis largely empirical and hard to
predict the effects of a minor change
Measuring local search
performance (1)
• Depth
how many clauses remain unsatisfied as
search proceeds
by averaging depth over all search steps as
an overall summary
Measuring local search
performance(2)
• Mobility
how rapidly a local search moves in search
space (while it tries to simultaneously stay
deep in the object)
by calculating the Hamming distance
between variable assignments that are k
steps apart and average this quantity over
the entire sequence
Measuring local search
performance(3)
• Coverage
how many systematically the search
explores the entire space
by computing the coverage rate to be (n –
max gap) / search steps where max gap is
the maximum Hamming distance between
unexplored assignment and the nearest
evaluated assignment
SDF: a new local search strategy
• Two main different components
(1) steepest descent in more informative
objective function
(2) multiplicative clauses re-weighting to
move out of local minima and travel to
promising new regions
• Weighted-score function
h(x, w) =  w(c)score(# xi ' s that satisfy c)
cxlauses
SDF procedure
• SDF ( ,  )
Flip the variable that leads to the greatest increase
in weighted-score function
• Re-weight ( ,  )
re-weight the unsatisfied clauses and re-normalize
the clause weights so that the resulting largest
difference is 
flatten the weight profile of the satisfied clauses by

shrinking 1   of the distance towards
their
common mean
Discussion
• Systematically reduce the number of flips
• Greater computational overhead per flip
Reference
[1]Schuurmans,D. and Southey,F.,Local
search characteristics of incomplete SAT
procedures, Proceedings of the Seventeenth
National Conference on Artificial
Intelligence (AAAI-2000),Austin,TX,July
2000.