A New Branching Heuristic for Propositional Satisfiability

A new algorithm of selecting branch variable is proposed,which is based on the research of propositional satisfiability algorithm. Firstly, the clause set is divided into three groups according to the length of the clause. Secondly,considering the relationship between the clause and literal dynamically and a heuristic function is defined,whose purpose is that literal has maximum function value will be selected. Examples show that the new algorithm can reduce the unnecessary search space,,then the efficiency of the whole solving is improved effectively.