Zur Seitenansicht
 

Titelaufnahme

Titel
Super-Blocked Clauses
VerfasserKiesl, Benjamin ; Seidl, Martina In der Gemeinsamen Normdatei der DNB nachschlagen ; Tompits, Hans ; Biere, Armin In der Gemeinsamen Normdatei der DNB nachschlagen
Erschienen in
Automated Reasoning. 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 July 2, 2016, Proceedings / Olivetti, Nicola, Cham, 2016, S. 45-61
Erschienen2016
Ausgabe
Accepted version
SpracheEnglisch
SerieLecture Notes in Computer Science ; 9706
DokumenttypAufsatz in einem Sammelwerk
Schlagwörter (EN)sat solving / preprocessing / propositional logic / blocked clauses / automated reasoning
Projekt-/ReportnummerAustrian Science Fund (FWF): W1255-N23, S11408-N23
ISBN978-3-319-40229-1
URNurn:nbn:at:at-ubtuw:3-3044 Persistent Identifier (URN)
DOI10.1007/978-3-319-40229-1_5 
Zugriffsbeschränkung
 Das Werk ist frei verfügbar
Dateien
Super-Blocked Clauses [0.31 mb]
Links
Nachweis
Klassifikation
Zusammenfassung (Englisch)

In theory and practice of modern SAT solving, clause-elimination procedures are essential for simplifying formulas in conjunctive normal form (CNF). Such procedures identify redundant clauses and faithfully remove them, either before solving in a preprocessing phase or during solving, resulting in a considerable speed up of the SAT solver. A wide number of effective clause-elimination procedures is based on the clause-redundancy property called blocked clauses. For checking if a clause C is blocked in a formula F, only those clauses of F that are resolvable with C have to be considered. Hence, the blocked-clauses redundancy property can be said to be local. In this paper, we argue that the established definitions of blocked clauses are not in their most general form. We introduce more powerful generalizations, called set-blocked clauses and super-blocked clauses, respectively. Both can still be checked locally, and for the latter it can even be shown that it is the most general local redundancy property. Furthermore, we relate these new notions to existing clause-redundancy properties and give a detailed complexity analysis.

Notiz