Backbone is a set of special variables of propositional formula, while it had important applications in 3-sat problems and SAT-based applications, so it is very important to solve the backbone efficiently. This paper proposed ID3_backbone algorithm for computing backbones of proposition formulae, this is because the principle of ID3 algorithm is to calculate the attribute information gain to determine the decision attribute, which can reduce the number of calls to the SAT solver. Experiments showed: ID3_Backbone algorithm can guarantee 75% accuracy under the condition of improving the efficiency, it propose an effective method to solve the problem of backbone set.
展开▼
