The Research On Backbone Algorithm

With the development of Integrated Circuits, the technology of the IC’s testingand verification has become more and more difficult, so that people have to changetheir traditional solving method, and through into a new field----SAT. The SATproblem was the first been proved NP problem. The SAT method can be widely usedin model checking、formal verification，equivalence checking，artificial intelligenceand so on. From1960to the present, SAT problem has been paying much attention,and a series of results has been achieved. Some low complexity but high efficiencySAT algorithm emerge as the times require. Among those, the most propoundalgorithm is DPLL. And the most famous SAT solver like Minisat,chaff，zchff are allbased on DPLL framework, they improve the efficiency of the algorithm by changethe constraint conditions or use some highly active heuristic strategy.There has a kind of Variables through the SAT problem whose values are thesame in all the satisfiability assignments (const to be0or const to be1), thosevariables are called backbone. The backbone problem can widely use to solveminimal unsatisfiable cores and the K-CNF SAT problem, verify the prime implicant.The bigger assemble of the backbone we have and the earlier we solve the backbone,the more efficient to solve the problem. There has several algorithm to find backbone,some are based on enumeration, some are based on iterative Sat testing, and others arebased on chunking block. We can combine those algorithms’ advantages anddisadvantages, On the basis of these algorithms, we can find several more efficientalgorithm to find backbone.The work of our paper is tried to combine those algorithm, learn from others’strong points and close the gap, set the different heuristic strategies and constraints,make the better interface between those algorithm, do its best to reflect the advantageof all those algorithm. In the implementation of our algorithm, we use an incrementSAT solver——PicoSAT. As a typical representative of increment SAT solver,PicoSAT can greatly enhance the efficiency of our algorithm. Through the experimental data we know that for all our algorithm can improve the solving speed tofind backbone.