2015/01/01 by Oliver Kullmann, João Marques‐Silva, Joao Marques-Silva · 12 citations
Computer Science · Mathematics · #Algorithm #Cardinality (data modeling) #Combinatorics #Computer science #Constraint Satisfaction and Optimization #Database #Discrete mathematics #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Mathematics #Oracle #Programming language #Property (philosophy) #Set (abstract data type) #Simple (philosophy) #Theoretical computer science #acm:03B05 #acm:05D99 #acm:68R99 #cs.DM #cs.DS #cs.LO #msc:03B05 #msc:05D99 #msc:68R99
paper · pdf · doi:10.1007/978-3-319-24318-4_11
published in Lecture notes in computer science, 138-155 (Springer Science+Business Media) · 18 pages; second version with editorial changes, to appear in LNCS for Theory and Applications of Satisfiability Testing - SAT 2015
openalex publication_date 2015/01/01 · arxiv created 2015/08/02 · arxiv updated 2016/04/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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, log2(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.