Computing maximal autarkies with few and simple oracle queries

TL;DR

This paper introduces new algorithms for computing maximal autarkies in clause-sets using minimal and simple SAT oracle queries, improving efficiency by leveraging modern SAT solver capabilities.

Contribution

It presents a novel algorithm combining autarky-resolution duality and SAT translations, reducing oracle calls needed for maximal autarky computation.

Findings

Logarithmic number of oracle calls with standard SAT oracle

Square root number of oracle calls with extended SAT oracle

Combines duality and SAT translation approaches for efficiency

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.