Book chapter 1126 views
Computing Maximal Autarkies with Few and Simple Oracle Queries
,
João Marques-Silva
Theory and Applications of Satisfiability Testing -- SAT 2015, Volume: 9340, Pages: 138 - 155
Swansea University Author:
Oliver Kullmann
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1007/978-3-319-24318-4_11
Abstract
We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments.We employ SAT solvers as oracles, using various capabil...
| Published in: | Theory and Applications of Satisfiability Testing -- SAT 2015 |
|---|---|
| Published: |
2015
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa26207 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
We consider the algorithmic task of computing a maximal autarky for a clause-set F, i.e., a partial assignment which satisfies every clause of F it touches, and where this property is destroyed by adding any non-empty set of further assignments.We employ SAT solvers as oracles, using various capabilities. Using the standard SAT oracle, log_2(n(F)) oracle calls suffice, where n(F) is the number of variables, but the drawback is that (translated) cardinality constraints are employed, which makes this approach less efficient in practice.Using an extended SAT oracle, motivated by the capabilities of modern SAT solvers, we show how to compute maximal autarkies with 2 n(F)^{1/2} simpler oracle calls. This novel algorithm combines the previous two main approaches, based on the autarky-resolution duality and on SAT translations. |
|---|---|
| Item Description: |
Lecture Notes in Computer Science 9340 |
| Keywords: |
Algorithms for hard problems, SAT |
| College: |
Faculty of Science and Engineering |
| Start Page: |
138 |
| End Page: |
155 |