Prefbones
This fork contains two improvements in the domain of backbones
- Implementation of Prefbones, proposed in "A Preference-based Approach to Backbone Computation with Application to Argumentation" by Previti and Järvisalo. This algorithm generally runs faster for real world instances, but slower for difficult instances like those used in the SAT competitions. This is available as pbb() in the Backbone class.
- Implementation of a stronger model reduction for the purpose of backbone computation, which is the intersection of all implicants in the found model (also known as unrotatable literals). This reduction disqualifies more literals per SAT call (depending on the instance of course) and also usually executes much faster than the prime implicant computation. This approach was described in "Algorithms for computing backbones of propositional formulae" by Marques-Silva,Janota and Lynce with an implementation hint described in section 4.1 of "Towards backbone computing: A Greedy-Whitening based approach" by Zhang,Zhang,Pu,Song and Li. I changed the backbone algorithms BB,IBB and my own to always use this reduction.
This code is an optimized reimplementation of what I created for my own master thesis (https://github.com/apothecarius/masterthesis). Feel free to give feedback before accepting this code into the main repository. I also plan to investigate whether it can be predicted reliably whether a preference based algorithm runs faster than ordinary algorithms (BB/IBB) by looking at the number of conflicts in the first SAT call.