No Cover Image

Conference Paper/Proceeding/Abstract 537 views

Generalising and Unifying SLUR and Unit-Refutation Completeness / Matthew Gwynne, Oliver Kullmann

SOFSEM 2013: Theory and Practice of Computer Science. LCNS, Volume: 7741, Pages: 220 - 232

Swansea University Author: Oliver Kullmann

Full text not available from this repository: check for access using links below.

Abstract

The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). W...

Full description

Published in: SOFSEM 2013: Theory and Practice of Computer Science. LCNS
ISSN: 0302-9743 1611-3349
Published: Springer 2013
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa13748
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: The class SLUR (Single Lookahead Unit Resolution) was introduced in [Schlipf, Annexstein, Franco, Swaminathan, 1995] as an umbrella class for efficient SAT solving. Balyo, Gursky, Cepek, Kucera, Vlcek in 2012 extended this class in various ways to hierarchies covering all of CNF (all clause-sets). We introduce a hierarchy SLUR_k which we argue is the natural “limit” of such approaches. The second source for our investigations is the class UC of unit-refutation complete clause-sets introduced in [del Val 1994]. Via the theory of (tree-resolution based) “hardness” of clause-sets as developed in ECCC-report, Annals-paper and [Ansotegui, Bonet, Levy, Manya, 2008], we obtain a natural generalisation UC_k, containing those clause-sets which are “unit-refutation complete of level k”, which is the same as having hardness at most k. Utilising the strong connections to (tree-)resolution complexity and (nested) input resolution, we develop fundamental methods for the determination of hardness (the level k in UCk ). A fundamental insight now is that SLUR_k = UC_k holds for all k. We can thus exploit both streams of intuitions and methods for the investigations of these hierarchies.
Keywords: algorithms, satisfiability, polynomial time, knowledge compilation
College: College of Science
Start Page: 220
End Page: 232