Sadly only the title of this talk fits the date. The backbone of a satisfiable formula is the set of literals that hold true in all satisfiable assignments. I will present the algorithmic details that allowed the impressive results of the recently developed backbone extractor CadiBack. We will focus especially on a new algorithm that allows to extract all backbones present in the Binary Implication Graph, allowing for improved performance when CadiBack is run in an anytime context.
Forschungs-