3.6 Different Learning Schemes

Different cuts separating decision variables from $ \Lambda$ and a conflict literal correspond to different learning schemes (see Figure 2). One can also create learning schemes based on cuts not involving conflict literals at all (Zhang et al., 2001), but the effectiveness of such schemes is not clear. These will not be considered here.

It is insightful to think of the nondeterministic scheme as the most general learning scheme. Here we pick the cut nondeterministically, choosing, whenever possible, one whose associated clause is not already known. Since we can repeatedly branch on the same last variable, nondeterministic learning subsumes learning multiple clauses from a single conflict as long as the sets of nodes on the reason side of the corresponding cuts form a (set-wise) decreasing sequence. For simplicity, we will assume that only one clause is learned from any conflict.

In practice, however, we employ deterministic schemes. The decision scheme (Zhang et al., 2001), for example, uses the cut whose reason side comprises all decision variables. rel-sat (Bayardo Jr., 1997) uses the cut whose conflict side consists of all implied variables at the current decision level. This scheme allows the conflict clause to have exactly one variable from the current decision level, causing an automatic flip in its assignment upon backtracking.

This nice flipping property holds in general for all unique implication points (UIPs) (Marques-Silva and Sakallah, 1996). A UIP of an implication graph is a node at the current decision level d such that any path from the decision variable at level d to the conflict variable as well as its negation must go through it. Intuitively, it is a single reason at level d that causes the conflict. Whereas rel-sat uses the decision variable as the obvious UIP, GRASP (Marques-Silva and Sakallah, 1996) and zChaff (Moskewicz et al., 2001) use FirstUIP, the one that is ``closest'' to the conflict variable. GRASP also learns multiple clauses when faced with a conflict. This makes it typically require fewer branching steps but possibly slower because of the time lost in learning and unit propagation.

The concept of UIP can be generalized to decision levels other than the current one. The 1UIP scheme corresponds to learning the FirstUIP clause of the current decision level, the 2UIP scheme to learning the FirstUIP clauses of both the current level and the one before, and so on. Zhang et al. (2001) present a comparison of all these and other learning schemes and conclude that 1UIP is quite robust and outperforms all other schemes they consider on most of the benchmarks.



Subsections
Journal of Artificial Intelligence Research 22 (2004). Copyright AI Access Foundation. All rights reserved.