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 here, and we are especially concerned with minimising the number of oracle calls. 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 \sqrt{n(F)}\) simpler oracle calls, by a novel algorithm, which combines the previous two main approaches, based on the autarky-resolution duality and on SAT translations.
This work is partially supported by SFI PI grant BEACON (09/IN.1/I2618), FCT grant POLARIS (PTDC/EIA-CCO/123051/2010) and national funds through FCT with reference UID/CEC/50021/2013.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (ed.): Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, February 2009
Brualdi, R.A., Shader, B.L.: Matrices of sign-solvable linear systems, volume 116 of Cambridge Tracts in Mathematics. Cambridge University Press (1995). ISBN 0-521-48296-8. doi:10.1017/CBO9780511574733
Davydov, G., Davydova, I.: Tautologies and positive solvability of linear homogeneous systems. Annals of Pure and Applied Logic 57(1), 27–43 (1992). doi:10.1016/0168-0072(92)90060-D
Even, S., Itai, A., Shamir, A.: On the complexity of timetable and multicommodity flow problems. SIAM Journal Computing 5(4), 691–703 (1976). doi:10.1137/0205048
Fleischner, H., Kullmann, O., Szeider, S.: Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science 289(1), 503–516 (2002). doi:10.1016/S0304-3975(01)00337-1
Franco, J., Van Gelder, A.: A perspective on certain polynomial-time solvable classes of satisfiability. Discrete Applied Mathematics 125(2–3), 177–214 (2003). doi:10.1016/S0166-218X(01)00358-4
Hall, F.J., Li, Z.: Sign pattern matrices. In: Hogben, L. (ed.), Handbook of Linear Algebra, Discrete Mathematics and Its Applications, pp. 33:1-33:21. Chapman & Hall/CRC, 2007. ISBN 1-58488-510-6. doi:10.1201/9781420010572.ch33
Heule, M.J.H., van Maaren, H.: Look-ahead based SAT solvers. In: Biere et al. [1], chapter 5, pp. 155–184. doi:10.3233/978-1-58603-929-5-155
Klee, V., Ladner, R.: Qualitative matrices: Strong sign-solvability and weak satisfiability. In: Greenberg, H.J., Maybee, J.S. (eds.), Computer-Assisted Analysis and Model Simplification, pp. 293–320 (1981). Proceedings of the First Symposium on Computer-Assisted Analysis and Model Simplification, University of Colorado, Boulder, Colorado, March 28, 1980. doi:10.1016/B978-0-12-299680-1.50022-7
Klee, V., Ladner, R., Manber, R.: Signsolvability revisited. Linear Algebra and its Applications 59, 131–157 (1984). doi:10.1016/0024-3795(84)90164-2
Büning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In : Biere et al. [1], chapter 11, pp. 339–401. doi:10.3233/978-1-58603-929-5-339
Krentel, M.W.: The complexity of optimization problems. Journal of Computer and System Sciences 36(3), 490–509 (1988). doi:10.1016/0022-0000(88)90039-6
Kullmann, O.: An application of matroid theory to the SAT problem. In: Proceedings of the 15th Annual IEEE Conference on Computational Complexity, pp. 116–124, July 2000. doi:10.1109/CCC.2000.856741
Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics 107, 99–137 (2000). doi:10.1016/S0166-218X(00)00262-6
Kullmann, O.: On the use of autarkies for satisfiability decision. In: Kautz, H., Selman, B. (ed.), LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001), volume 9 of Electronic Notes in Discrete Mathematics (ENDM), pp. 231–253. Elsevier Science, June 2001. doi:10.1016/S1571-0653(04)00325-7
Kullmann, O.: Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics 130, 209–249 (2003). doi:10.1016/S0166-218X(02)00406-7
Kullmann, O.: Polynomial time SAT decision for complementation-invariant clause-sets, and sign-non-singular matrices. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 314–327. Springer, Heidelberg (2007)
Kullmann, O.: Constraint satisfaction problems in clausal form I: Autarkies and deficiency. Fundamenta Informaticae 109(1), 27–81 (2011). doi:10.3233/FI-2011-428
Kullmann, O.: Constraint satisfaction problems in clausal form II: Minimal unsatisfiability and conflict structure. Fundamenta Informaticae 109(1), 83–119 (2011). doi:10.3233/FI-2011-429
Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22–35. Springer, Heidelberg (2006)
Kullmann, O., Zhao, X.: On variables with few occurrences in conjunctive normal forms. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 33–46. Springer, Heidelberg (2011)
Kullmann, O., Zhao, X.: Bounds for variables with few occurrences in conjunctive normal forms. Technical Report arXiv:1408.0629v3 [math.CO], arXiv, November 2014. http://arxiv.org/abs/1408.0629
Lee, G.-Y., Shader, B.L.: Sign-consistency and solvability of constrained linear systems. The Electronic Journal of Linear Algebra, 4:1–18, August 1998. http://emis.matem.unam.mx/journals/ELA/ela-articles/4.html
Li, C.M., Manyà, F.: MaxSAT, hard and soft constraints. In: Biere et al. [1], chapter 19, pp. 613–631. doi:10.3233/978-1-58603-929-5-613
Liffiton, M.H., Sakallah, K.A.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 182–195. Springer, Heidelberg (2008)
Marques-Silva, J., Ignatiev, A., Morgado, A., Manquinho, V., Lynce, I.: Efficient autarkies. In: Schaub, T., Friedrich, G., O’Sullivan, B. (ed.), 21st European Conference on Artificial Intelligence (ECAI 2014), volume 263 of Frontiers in Artificial Intelligence and Applications, pp. 603–608. IOS Press (2014). doi:10.3233/978-1-61499-419-0-603
Marques-Silva, J., Janota, M.: On the query complexity of selecting few minimal sets. Technical Report TR14-031, Electronic Colloquium on Computational Complexity (ECCC), March 2014. http://eccc.hpi-web.de/report/2014/031/
Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere et al. [1], chapter 4, pp. 131–153. doi:10.3233/978-1-58603-929-5-131
McCuaig, W.: Pólya’s permanent problem. The Electronic Journal of Combinatorics, 11, 2004. #R79, 83 p. http://www.combinatorics.org/ojs/index.php/eljc/article/view/v11i1r79
Monien, B., Speckenmeyer, E.: Solving satisfiability in less than \(2^n\) steps. Discrete Applied Mathematics 10(3), 287–295 (1985). doi:10.1016/0166-218X(85)90050-2
Okushi, F.: Parallel cooperative propositional theorem proving. Annals of Mathematics and Artificial Intelligence 26(1–4), 59–85 (1999). doi:10.1023/A:1018946526109
Papadimitriou, C.H., Wolfe, D.: The complexity of facets resolved. Journal of Computer and System Sciences 37(1), 2–13 (1988). doi:10.1016/0022-0000(88)90042-6
Robertson, N., Seymour, P.D., Thomas, R.: Permanents, Pfaffian orientations, and even directed circuits. Annals of Mathematics 150(3), 929–975 (1999). doi:10.2307/121059
Roussel, O., Manquinho, V.: Pseudo-boolean and cardinality constraints. In: Biere et al. [1], chapter 22, pp. 695–733. doi:10.3233/978-1-58603-929-5-695
Samuelson, P.A.: Foundations of Economic Analysis. Harvard University Press (1947)
Szeider, S.: Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable. Journal of Computer and System Sciences 69(4), 656–674 (2004). doi:10.1016/j.jcss.2004.04.009
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Kullmann, O., Marques-Silva, J. (2015). Computing Maximal Autarkies with Few and Simple Oracle Queries. In: Heule, M., Weaver, S. (eds) Theory and Applications of Satisfiability Testing -- SAT 2015. SAT 2015. Lecture Notes in Computer Science(), vol 9340. Springer, Cham. https://doi.org/10.1007/978-3-319-24318-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-24318-4_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24317-7
Online ISBN: 978-3-319-24318-4
eBook Packages: Computer ScienceComputer Science (R0)