Branching Strategy Selection Approach Based on Vivification Ratio
This work addresses a specific challenge in SAT solving for improving solver performance on diverse instance types, representing an incremental advancement.
The paper tackles the problem of selecting between two effective but instance-dependent branching strategies (LRB and VSIDS) in SAT solvers by proposing a selection approach based on the vivification ratio, which significantly increases the number of solved instances, solving over 16 more instances on a 2020 benchmark.
The two most effective branching strategies LRB and VSIDS perform differently on different types of instances. Generally, LRB is more effective on crafted instances, while VSIDS is more effective on application ones. However, distinguishing the types of instances is difficult. To overcome this drawback, we propose a branching strategy selection approach based on the vivification ratio. This approach uses the LRB branching strategy more to solve the instances with a very low vivification ratio. We tested the instances from the main track of SAT competitions in recent years. The results show that the proposed approach is robust and it significantly increases the number of solved instances. It is worth mentioning that, with the help of our approach, the solver Maple\_CM can solve more than 16 instances for the benchmark from the 2020 SAT competition.