Skip to main content
SpringerLink
Log in

Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank

  • Conference paper
Theory and Applications of Satisfiability Testing (SAT 2004)

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

Abstract

Combining graph theory and linear algebra, we study SAT problems of low “linear algebra complexity”, considering formulas with bounded hermitian rank. We show polynomial time SAT decision of the class of formulas with hermitian rank at most one, applying methods from hypergraph transversal theory. Applications to heuristics for SAT algorithms and to the structure of minimally unsatisfiable clause-sets are discussed.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Berge, C.: Hypergraphs: Combinatorics of Finite Sets. North-Holland Mathematical Library, vol. 45. North Holland, Amsterdam (1989), (ISBN 0 444 87489 5; QA166.23.B4813 1989)

    Google Scholar 

  2. Bunch, J.R., Kaufman, L.: Some stable methods for calculating inertia and solving symmetric linear systems. Mathematics of Computation 31(137), 163–179 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  3. Büning, H.K., Zhao, X.: On the structure of some classes of minimal unsatisfiable formulas. Discrete Applied Mathematics 130, 185–207 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  4. Cvetković, D.M., Doob, M., Gutman, I., Torgašev, A.: Recent Results in the Theory of Graph Spectra. Annals of Discrete Mathematics, vol. 36. North-Holland, Amsterdam (1988), (ISBN 0-444-70361-6; QA166.R43 1988)

    Google Scholar 

  5. Eiter, T.: Exact transversal hypergraphs and application to boolean μ-functions. Journal of Symbolic Computation 17, 215–225 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  6. Eiter, T., Gottlob, G.: Identifying the minimal transversals of a hypergraph and related problems. SIAM Journal on Computing 24(6), 1278–1304 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  7. Fredman, M.L., Khachiyan, L.: On the complexity of dualization of monotone disjunctive normal forms. Journal of Algorithms 21(3), 618–628 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  8. Graham, R.L., Pollak, H.O.: On the addressing problem for loop switching. Bell System Technical Journal 50(8), 2495–2519 (1971)

    MATH  MathSciNet  Google Scholar 

  9. Gregory, D.A., Watts, V.L., Shader, B.L.: Biclique decompositions and hermitian rank. Linear Algebra and its Applications 292, 267–280 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  10. Kullmann, O.: Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Technical Report TR99-041, Electronic Colloquium on Computational Complexity (ECCC) (October 1999)

    Google Scholar 

  11. Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science 223(1-2), 1–72 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96-97(1-3), 149–176 (1999)

    Article  MathSciNet  Google Scholar 

  13. Kullmann, O.: On the conflict matrix of clause-sets. Technical Report CSR 7-2003, University of Wales Swansea, Computer Science Report Series (2003)

    Google Scholar 

  14. Kullmann, O.: The combinatorics of conflicts between clauses. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 426–440. Springer, Berlin (2004), (ISBN 3-540-20851-8)

    Google Scholar 

  15. Kullmann, O.: The conflict matrix of (multi-)clause-sets — a link between combinatorics and (generalised) satisfiability problems. In: Preparation; continuation of [13] (2004)

    Google Scholar 

  16. Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Annals of Mathematics and Artificial Intelligence 40(3-4), 303–352 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  17. Kullmann, O., Luckhardt, H.: Deciding propositional tautologies: Algorithms and their complexity. Preprint, p. 82 (January 1997)

    Google Scholar 

  18. Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures. Preprint, p. 71 (December 1998)

    Google Scholar 

  19. Petrović, M.M.: The spectrum of an infinite labelled graph. Master’s thesis, University Beograd, Faculty of Science (1981)

    Google Scholar 

  20. Torgašev, A.: Graphs with the reduced spectrum in the unit interval. Publ. Inst. Math (Beograd) 36(50), 15–26 (1984)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departament de Llenguatges i Sistemes Informàtics, Universitat Politécnica de Catalunya, Barcelona, Spain

    Nicola Galesi

  2. Computer Science Department, University of Wales Swansea, Swansea, SA2 8PP, UK

    Oliver Kullmann

Authors
  1. Nicola Galesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oliver Kullmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of British Columbia Vancouver, V6T 1Z4, B.C., Canada

    Holger H. Hoos

  2. Computational Logic Laboratory, Simon Fraser University, Burnaby, BC, Canada

    David G. Mitchell

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Galesi, N., Kullmann, O. (2005). Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing. SAT 2004. Lecture Notes in Computer Science, vol 3542. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527695_8

Download citation

  • DOI: https://doi.org/10.1007/11527695_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-27829-0

  • Online ISBN: 978-3-540-31580-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation