Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?

Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin

doi:10.24963/ijcai.2017/687

Notice
This item was automatically migrated from a legacy system. It's data has not been checked and might not meet the quality criteria of the present system.

DC Field

Value

Language

dc.contributor.author

Kiesl, Benjamin

dc.contributor.author

Seidl, Martina

dc.contributor.author

Tompits, Hans

dc.contributor.author

Biere, Armin

dc.contributor.editor

Bacchus, Fahiem

dc.date.accessioned

2022-08-04T16:48:49Z

dc.date.available

2022-08-04T16:48:49Z

dc.date.issued

2017

dc.identifier.citation

<div class="csl-bib-body"> <div class="csl-entry">Kiesl, B., Seidl, M., Tompits, H., & Biere, A. (2017). Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood? In F. Bacchus (Ed.), <i>Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence</i>. https://doi.org/10.24963/ijcai.2017/687</div> </div>

dc.identifier.uri

http://hdl.handle.net/20.500.12708/57274

dc.description.abstract

Clause-elimination techniques that simplify formulas by removing redundant clauses play an important role in modern SAT solving. Among the types of redundant clauses, blocked clauses are particularly popular. For checking whether a clause C is blocked in a formula F, one only needs to consider the so-called resolution neighborhood of C, i.e., the set of clauses that can be resolved with C. Because of this, blocked clauses are referred to as being locally redundant. In this paper, we discuss powerful generalizations of blocked clauses that are still locally redundant, namely set-blocked clauses and super-blocked clauses. We furthermore present complexity results for deciding whether a clause is set-blocked or super-blocked.

dc.subject

propositional logic

dc.subject

sat solving

dc.subject