The problem of propositional satisfiability (SAT) has found a number of applications in both theoretical and practical computer science. However, in many applications, knowing a formulae's satisfiability alone is not enough to solve problems. Often, some other characteristics of formulae need to be known. In 1997, the definition of backbone occur - a set of variables which are true in any assignment of SAT, which starts the research of solution structure. Gradually, backbone has been recognized having great effect in rapidly solving intelligent planning and automated reasoning problems. First of all, this article reviews three existing algorithms for computing backbone, finding that no algorithm uses solved backbone as information. Based on this idea, we bring up a new algorithm for computing backbone of propositional formulae using solved backbone information. This article utilizes latest SAT competition data on original fastest algorithm (one test per time of 30 chuck) and the new algorithm. According to the experiment results, the new algorithm can have 10% advance on rate at the set of data which contain 80% or more chuck so it has practical application value.
展开▼
