Skip to main content

New Results in Cutting Seriation for Approximate #SAT

  • Chapter
Data Analysis

Abstract

The general problem discussed here concerns the approximation of the number of solutions of a boolean formula in conjunctive normal form F. Results previously obtained (Rouat (1999), Lerman and Rouat (1999)) are reconsidered and completed. Our method is based on the general principle “divide to resolve”. The division is achieved by cutting a seriation built on an incidence data table associated with F. In this, the independence probability concept is finely exploited. Theoretical justification and intensive experimentation validate the considerable reduction of the computational complexity obtained by our method.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

  • ANDRÉ, P. and DUBOIS, O. (1992): Utilisation de l’espérance du nombre de solutions afin d’optimiser la résolution du problème SAT. C.R. de l’Académie des Sciences, Paris, 315, 217–220.

    Google Scholar 

  • BAILLEUX, O. and CHABRIER, J.J. (1996): Approximate resolution of hard numbering problems. In: AAAI Thirteenth National Conference on Artificial Intelligence, 169–174.

    Google Scholar 

  • COOK, S.A. (1971): The complexity of theorem-proving procedures. In: 3rd Annual ACM Symposium on the Theory of Computing, 151–158.

    Google Scholar 

  • DAVIS, M. and PUTNAM, H. (1960): A computing procedure for quantification theory. Journal of the ACM, vol. 7, 3, 201–215.

    Article  Google Scholar 

  • DUBOIS, O. (1991): Counting the number of solutions for instances of satisfiability. Theoretical Computer Science, 81, 49–64.

    Article  Google Scholar 

  • KARP, R.M. and LUBY, M. (1983): Monte-carlo algorithms for enumeration and reliability problems. In: 24th IEEE Symposium of Foundations of Computer Science, 56–64.

    Google Scholar 

  • LEREDDE, H. (1979): La méthode des pôles d’attraction, la méthode des pôles d’agrégation; deux nouvelles familles d’algorithmes en classification automatique et sériation. PhD thesis, Université de Paris VI.

    Google Scholar 

  • LERMAN, I.C. (1972): Analyse du phénomène de la “sériation” à partir d’un tableau d’incidence. Mathématiques et Sciences Humaines, 38, 39–57.

    Google Scholar 

  • LERMAN, I.C. (1995): Statistical reduction of the satisfiability problem by means of a classification method. Data Science and its Application, Academic Press, 219–234.

    Google Scholar 

  • LERMAN, I.C. and ROUAT, V. (1999): Segmentation de la sériation pour la résolution de #SAT. Mathématiques, Informatique et Sciences Humaines, 147, 113–134.

    Google Scholar 

  • LOZINSKII, E.L. (1992): Counting propositional models. Information Processing Letters, 41, 327–332.

    Article  Google Scholar 

  • MARCOTORCHINO, F. (1987): Block seriation problems: a unified approach. Applied Stochastic Models and Data Analysis, vol. 3, 2, 73–91.

    Article  Google Scholar 

  • PAPADIMITRIOU, C.H. (1994): Computational complexity. Addison Wesley.

    Google Scholar 

  • ROUAT, V. (1999): Validité de l’approche classification dans la réduction statistique de la complexité de #SAT. PhD thesis, Université de Rennes 1, 1999.

    Google Scholar 

  • ROUAT, V. and LERMAN, I.C. (1997): Utilisation de la sériation pour une résolution approchée du problème #SAT. In: JNPC’97, résolution pratique de problèmes NP-complets, 55–60.

    Google Scholar 

  • ROUAT, V. and LERMAN, I.C. (1998): Problématique de la coupure dans la résolution de #SAT par sériation. In: JNPC’98, résolution pratique de problèmes NP-complets, 109--114.

    Google Scholar 

  • SIMON, J.C. and DUBOIS, O. (1989): Number of solutions of satisfiability instances — applications to knowledge bases. International Journal of Pattern Recognition and Artificial Intelligence, vol. 3, 1, 53–65.

    Article  Google Scholar 

  • TODA, S. (1989): On the computational power of PP and ⊕P. In: 30th Annual Symposium on Foundations of Computer Science, 514–519.

    Chapter  Google Scholar 

  • VALIANT, L.G. (1979): The complexity of enumeration and reliability problems. SIAM Journal on Computing, vol. 8, 3, 410–421.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin · Heidelberg

About this chapter

Cite this chapter

Lerman, I.C., Rouat, V. (2000). New Results in Cutting Seriation for Approximate #SAT. In: Gaul, W., Opitz, O., Schader, M. (eds) Data Analysis. Studies in Classification, Data Analysis, and Knowledge Organization. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-58250-9_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-58250-9_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67731-4

  • Online ISBN: 978-3-642-58250-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics