Experimental analysis of backbone computation algorithms

Abstract. In a number of applications, it is not sufficient to decide whether a given propositional formula is satisfiable or not. Often, one needs to infer specific properties about a formula. This paper focuses on the computation of backbones, which are variables that have the same value in all models of a Boolean formula. Backbones find theoret-ical applications in characterization of SAT problems but they also find practical applications in product configuration or fault localization. This paper presents an extensive evaluation of existing backbone computation algorithms on a large set of benchmarks. This evaluation shows that it is possible to compute the set of backbones for a large number of instances and it also demonstrates that a large number of backbones appear in practical instances.