Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver

Abstract

For the SAT solver,most popular branch variable decision-making strategies are based on the variable activity evaluation of conflict.The unassigned variable with the maximum activity is selected as the decision variable,and the most recent conflict is solved first.However,they all ignore the impact of the number of clauses containing decision variables on the Boolean constraint propagation (BCP).To solve this problem,this paper proposes a branch variable decision strategy (VDALCD) based on the learning clause deletion strategy,which reduces the activity of variables in the deleted clause when the clause is deleting.Based on the VDALCD strategy,Glucose4.1 and MapleLCMDistChronoBT-DL-v2.1 are improved to solvers Glucose4.1_VDALCD and Maple-DL_VDALCD.This paper uses 2018 and 2019 SAT international competition questions as benchmark test cases to compare the improved version with the original version of the solver.The experimental results show that Gluose4.1_VDALCD finds out 26 more examples than Gluose4.1,an increase of 15.5% in the 2018 example test.In the 2019 example test,Maple-DL_VDALCD finds out 17 more examples than MapleLCMDistChronoBT-DL-v2.1,an increase of 7.6%.

Keywords

• activity|learnt clause|satisfiability problem|learnt clause deletion strategy|complete algorithms