DPLL-待修改1

Therefore, taking an action in a state results in two (possibly absorbing) new states. This

one-to-two state transition violates the standard MDP definition, but it can be thought of as

cloning the MDP and creating one copy for each transition. The two copies continue

independently thereafter. The immediate cost paid for choosing a branching rule is computed in

two different ways. The total number of search nodes that results from unit propagations,

between the original and the two new states, is the node cost paid for the decision at the original

node. That is the immediate cost for choosing the branching rules MAXO, MOMS, MAMS, and

JW. The other three branching rules perform trial partial searches to determine the branching

variable. The total number of nodes created during these trial searches is added to the above