• Authors: Mikoláš Janota
  Contributors: J. Marques-Silva and I. Lynce
• Contact: mikolas DOT-GOES-HERE janota AT-SIGN-GOES-HERE gmail DOT-GOES-HERE com

The tool minibones computes the backbone literals of a given formula. Backbone literals are such literals that are true in all models of the formula. Different names are used in literature, e.g. necessary assignments. The tool implements techniques described in [1,2].

source-code on github
Fork by Armin Biere, resolving some compilation issues (March 2023)
linux 64 bit binaries, 0.7
linux 64 bit binaries, 0.5

Results for the AI-COM 2015 article.

(C) 2012 Mikolas Janota

minibones is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

minibones is free for noncommercial use.

[1] Algorithms for Computing Backbones of Propositional Formulae [preprint] [ee] Mikoláš Janota, Inês Lynce, and Joao Marques-Silva. RCRA 2012 AI-Com special issue, 2015

[2] On Computing Backbones of Propositional Theories Joao Marques-Silva, Mikoláš Janota, and Inês Lynce. The 19th European Conference on Artificial Intelligence (ECAI '10).

---

Last updated: Mar 06, 2023 11:52:34 PM