Research of Branching Heuristic Strategy for Implied Literal in Shortest Clause for SAT Problem
Rong Hu · 2017
Branching heuristic strategy plays a very important role in CDCL-based algorithms.In this paper, we propose a new branching heuristic inspired by the new dynamic phase selection policy used to improve Glucose 2.0.As it says, SAT solvers now use a new data structure - observing to text structure. When a clause contains implied literal, it automatically assigns the corresponding value, which can be applied here. Its advantage is the use of the integrity of the SAT solver. The main idea of this strategy is to give priority to the shortest clause, and also to reduce the size of the long clause, making it a shorter clause.