I understand that by being clever about the way we navigate the search space of the SAT problem we're going to get better performance than by randomly choosing and testing solutions, though of course both methods have $O(2^n)$ time complexity. What are the specific reasons that DPLL gives better performance than brute-force (sequentially testing solutions from FALSE-FALSE-FALSE.... to TRUE-TRUE-TRUE....)?
Asked By : René G
Answered By : Kyle Jones
Local (stochastic) search is all about clever navigation of the search space. DPLL's advantage is pruning the search space of large swaths of assignments that provably cannot satisfy the formula. DPLL does this by incrementally building partial assignments (some variables assigned values, some left unassigned), applying the unit propagation and pure literal rules and then checking if the resulting formula is trivially unsatisfiable. If the simplified formula implied by the partial assignment contains an empty clause, DPLL need not try assigning values to the remaining unassigned variables since the empty clause represents a clause that can never be satisfied under the partial assignment. The time saved is exponential to the number of unassigned variables, and those skipped assignments are where DPLL improves on brute force sequential search.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/33632
0 comments:
Post a Comment
Let us know your responses and feedback