On Computing Backbones of Propositional Theories

10 years 1 days ago
On Computing Backbones of Propositional Theories
Backbones of propositional theories are literals that are true in every model. Backbones have been used for characterizing the hardness of decision and optimization problems. Moreover, backbones find other applications. For example, backbones are often identified during product configuration. Backbones can also improve the efficiency of solving computational problems related with propositional theories. These include model enumeration, minimal model computation and prime implicant computation. This paper investigates algorithms for computing backbones of propositional theories, emphasizing the integration of these algorithms with modern SAT solvers. Experimental results, obtained on representative problem instances, indicate that the proposed algorithms are effective in practice and can be used for computing the backbones of large propositional theories. In addition, the experimental results indicate that propositional theories can have large backbones, often representing a significant...
João Marques-Silva, Mikolás Janota,
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where ECAI
Authors João Marques-Silva, Mikolás Janota, Inês Lynce
Comments (0)