Title: Super-Blocked Clauses
Language: English
Authors: Kiesl, Benjamin 
Seidl, Martina 
Tompits, Hans 
Biere, Armin 
Keywords: sat solving; preprocessing; propositional logic; blocked clauses; automated reasoning
Issue Date: 2016
Abstract: 
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.
URI: https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3044
http://hdl.handle.net/20.500.12708/356
Library ID: AC11362487
ISBN: 9783319402291
Organisation: E192 - Institut für Informationssysteme 
Publication Type: Inproceedings
Konferenzbeitrag
Appears in Collections:Conference Paper

Files in this item:

File Description SizeFormat
Kiesl Benjamin - 2016 - Super-Blocked Clauses.pdf321.16 kBAdobe PDFThumbnail
 View/Open
Show full item record

Page view(s)

1
checked on Mar 29, 2021

Download(s)

1
checked on Mar 29, 2021

Google ScholarTM

Check


Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.