A Branching Strategy Based on the Length of Learnt Clause

摘要

Decision strategy is as a great part in the CDCL algorithm, so the efficient branching strategy is one of the key features of the SAT problem solver. Originally some basic knowledge and concepts are brought in, then there are some concrete steps of the branching variable heuristic algorithm-VSIDS algorithm, finally based on the relationship between the learnt clause length and the decision level, a new branching strategy presents,which is also based on VSIDS strategy, the new branching strategy makes the difference between the decision levels of variables involved in conflict analysis and the the current conflict level as the conflict adding score conditions, and considering the learnt clause length as the adding score, in order to enhance the efficiency of variable selection, some examples of the VSIDS strategy and the new strategy are analyzed lastly.