Generalising Unit-Refutation Completeness and SLUR via Nested Input Resolution - Oliver Kullmann (Journal of Automated Reasoning, 2014)
The class SLUR has been introduced in 1995 as an umbrella class for fast SAT solving, while the class UC has been introduced in 1994 for the purpose of knowledge compilation. We now show that SLUR = UC holds, and this in a strongly generalised context, embedding these classes into a rich theory. Fundamental is the notion of "hardness", which is explored here systematically.