Skip to main content
SpringerLink
Log in

Computing Maximal Autarkies with Few and Simple Oracle Queries

  • Conference paper
  • First Online:
Theory and Applications of Satisfiability Testing -- SAT 2015 (SAT 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9340))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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

    Google Scholar 

  2. 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

  3. 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

    Article  MathSciNet  MATH  Google Scholar 

  4. 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

    Article  MathSciNet  MATH  Google Scholar 

  5. 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

    Article  MathSciNet  MATH  Google Scholar 

  6. 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

    Article  MathSciNet  MATH  Google Scholar 

  7. 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

  8. 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

  9. 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

  10. 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

    Article  MathSciNet  MATH  Google Scholar 

  11. 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

  12. 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

    Article  MathSciNet  MATH  Google Scholar 

  13. 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

  14. Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics 107, 99–137 (2000). doi:10.1016/S0166-218X(00)00262-6

    Article  MathSciNet  MATH  Google Scholar 

  15. 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

  16. 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

    Article  MathSciNet  MATH  Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. 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

    MathSciNet  MATH  Google Scholar 

  19. 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

    MathSciNet  MATH  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. 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

  23. 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

  24. 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

  25. 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)

    Chapter  Google Scholar 

  26. 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

  27. 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/

  28. 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

  29. 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

  30. 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

    Article  MathSciNet  MATH  Google Scholar 

  31. Okushi, F.: Parallel cooperative propositional theorem proving. Annals of Mathematics and Artificial Intelligence 26(1–4), 59–85 (1999). doi:10.1023/A:1018946526109

    Article  MathSciNet  MATH  Google Scholar 

  32. 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

    Article  MathSciNet  MATH  Google Scholar 

  33. 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

    Article  MathSciNet  MATH  Google Scholar 

  34. 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

  35. Samuelson, P.A.: Foundations of Economic Analysis. Harvard University Press (1947)

    Google Scholar 

  36. 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

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Swansea University, Swansea, UK

    Oliver Kullmann

  2. INESC-ID, IST, University of Lisbon, Lisbon, Portugal

    João Marques-Silva

Authors
  1. Oliver Kullmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. João Marques-Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to João Marques-Silva .

Editor information

Editors and Affiliations

  1. Algorithms, University of Texas, Austin, Texas, USA

    Marijn Heule

  2. Trusted Systems Research Group, Fort Meade, Texas, USA

    Sean Weaver

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation