Branching Strategy Selection Approach Based on Vivification Ratio

TL;DR

This paper introduces a new method for selecting branching strategies in SAT solvers based on vivification ratio, improving problem-solving efficiency and solving more instances from recent SAT competitions.

Contribution

A novel strategy selection approach using vivification ratio to dynamically choose between LRB and VSIDS in SAT solving.

Findings

Significantly increases the number of solved instances.

Robust approach effective on recent SAT competition benchmarks.

Enables Maple_CM to solve 16+ more instances from 2020 SAT benchmark.

Abstract

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.