Recent work has shown that SAT can be theoretically more powerful than heuristic search provided the heuristic used by search is implemented as a set of clauses on which unit propagation simulates the evaluation of the heuristic. The h~(max) heuristic has been shown to be implemented trivially by the empty set of clauses. This paper presents an implementation of h~m, a generalization of h~(max).
展开▼
