Counting for Satisfiability by Inverting Resolution

• Andrei, Ş. (1995). (submitted: 1993, reported in talks: 1991) The Determinant of the Boolean Formulae, Analele Universit a _ t ii Bucureşti, Informatic a Ano. XLIV, 83–92, Rom a nia, URL: http: //www. infoiasi. ro/stefan/anale95. pdf.

  Google Scholar 

• Andrei, Ş. (1999). Weak Equivalence in Propositional Calculus. In Todiraşcu, A. (ed. ), Proceedings of European Summer School on Logic, Language and Information, August 9–20, 79–89, Universiteit Utrecht: The Netherlands, URL-s: http://www.let.uu.nl/esslli/student-session.html, and http://www.folli.uva.nl/CD/1999/ library/pdf/andrei.pdf.

  Google Scholar 

• Andrei, Ş., Kudlek, M., & Masalagiu, C. (2001). The Resolution Principle. Complexity Estimations for the Class of Propositional Calculus Formulae, Research Report FBI-HH-B-233, 1–16. Fachbereich Informatik, Universitat Hamburg.

• Andrei, Ş, Grigoraş, G., Kudlek, M. & Masalagiu, C. (2001). On the Complexity of Propositional Calculus Formulae. Analele Ştiint ¸ifice ale Facult a t ¸ii de Informatic a Tomul X, 27–43. ''A. I. Cuza ''University: Iaşi, România, URL: http: //www. infoias. ro/stefan/anale2001. pdf.

  Google Scholar 

• Birbaum, E. & Lozinskii, E. L. (1999). The Good Old Davis-Putnam Procedure Helps Counting Models. Journal of Artificial Intelligence Research 10: 457–477.

  Google Scholar 

• Beame, P., Karp, R., Pitassi, T. & Saks, M. (2002). The Efficiency of Resolution and Davis-Putnam Procedures, SIAM Journal of Computing 31(4): 1048–1075.

  Google Scholar 

• Chang, C. L. & Lee, R. C. T. (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press: New York.

  Google Scholar 

• Cheng, A. M. K. (2002). Real-time systems. Scheduling, Analysis, and Verication. Wiley Interscience.

• Clay Mathematics Institute: (2000). http: //www. claymath. org/Millennium_Prize_Problems/P_vs_NP/

• Cook, S. A. (1971). The complexity of theorem-proving procedures, Proceeding of the Third Annual ACM Symposium Theory of Computing, 151–158.

• De Raedt, L. (1992) Interactive Theory Revision: An Inductive Logic Programming Approach. Academic Press: London.

  Google Scholar 

• Davis, M. & Putnam, H. (1960). A Computing Procedure for Quanti cation Theory. Journal of the ACM 7: 201–215.

  Google Scholar 

• Dahllof, V., Jonsson, P. & Wahlstrom, M. (2002). Counting Satisfying Assignments in 2-SATand 3-SAT, COCOON-2002 LNC82387, Ibarra, O. & Zhang, L. (eds.), 535–543.

• Deng, X., Lee, C. H., Zhao, Y. & Zhu, H. (2002). (2+f(n))-SAT and Its Properties, COCOON-2002 LNC8 2387, Ibarra, O. & Zhang, L. (eds. ), 28–36.

• Dowling, W. F. & Gallier, J. H. (1984). Linear-time Algorithms for Testing the Satis-ability of Propositional Horn Formulae, Journal of Logic Programming 3: 267–284.

  Google Scholar 

• Dubois, O. (1991). Counting the Number of Solutions for Instances of Satisi ability. Theoretical Computer Science 81: 49–64.

  Google Scholar 

• Gallier, J. (1987). Logic for Computer Science (Foundations of Automatic Theorem Proving). Harper and Row Publishers: New York.

  Google Scholar 

• Garey, M. R. & Johnson, D. S. (1979). Computers and Intractability: A Guide to the Theory of NP-completeness. Freeman, San Francisco: CA.

  Google Scholar 

• Iwana, K. (1989). CNF Satis ability Test by Counting and Polynomial Average Time, Siam Journal of Computing 18(2): 385–391.

  Google Scholar 

• Karp, R. M. (1972). Reducibility Among Combinatorial Problems. In R. E. Miller & J. W. Thatcher (eds. ), Complexity of Computer Computations, 85–103. Plenum Press: NewYork.

  Google Scholar 

• Jahanian, F. & Mok, A. (1986). Safety Analysis of Timing Properties in Real-Time Systems. IEEE Transactions on Software Engineering SE-12(9): 890–904.

  Google Scholar 

• Jahanian, F. & Mok, A. (1987). A Graph-Theoretic Approach for Timing Analysis and its Implementation. IEEE Transactions on Computers C-36, (8): 961–975.

  Google Scholar 

• Lavrač, N. & Džeroski, S. (1994). Inductive Logic Programming: Techniques and Applications. Ellis Horwood: New York.

  Google Scholar 

• Levin, L. A. (1973). (submitted: 1972, reported in talks: 1971) Universal Search Problems. Problemy Peredachi Informatsii = Problems of Information Transmission 9 (3): 265–266.

  Google Scholar 

• Lloyd, J. W. (1984). Foundations of Logic Programming. Springer-Verlag: Berlin, Germany.

  Google Scholar 

• Lozinskii, E. (1992). Counting Propositional Models. Information Processing Letters 41 (6): 327–332.

  Google Scholar 

• Masalagiu, C. & Andrei, Ş. (2000). Duality in Resolution, Analele Universit a _ t ii Bu-cure şti, Informatic a Ano. XLIX, 97–112. Rom a nia, URL: http: //www. infoiasi. ro/ stefan/anale2000. pdf.

  Google Scholar 

• Muggleton, S. & De Raedt, L. (1994). Inductive logic programming: Theory and Methods. Journal of Logic Programming, 19 (20): 629–679.

  Google Scholar 

• Muggleton, S. (1992). Inductive Logic Programming. (ed. ). Academic Press: London.

  Google Scholar 

• Muggleton, S. (1995). Inverse Entailment and Progol. New Generation Computing, Special Issue on Inductive Logic Programming, 13 (3–4): 245–286.

  Google Scholar 

• Page, D. (2000). ILP: Just Do It. Lloyd, J. Dahl, Kerber, Lau, Palamidissi, Pereira, Sagiv, Stuckey (eds), 25–40. Proceedings of Computational Logic, Berlin: Springer, LNAI 1861, Also appears in Proceedings of ILP '2000, Cussens J. & Frisch, A. (eds), 3–18. Berlin: Springer; LNAI 1866.

  Google Scholar 

• Papadimitriou, C. H. (1994). Computational Complexity. Addison-Wesley: USA.

  Google Scholar 

• Purdom, P. 1989, Random Satis ability Problems, International Workshop on Discrete Algorithms and Complexity 89-AL-12, 253–259. IECE Japan.

  Google Scholar 

• Robinson, J. A. (1965). A Machine Oriented Logic Based on the Resolution Principle. Journal of the ACM 12: 23–41.

  Google Scholar 

• Roth, D. On the Hardness of Approximate Reasoning. Artificial Intelligence 82: 273–302.

• Simon, J. (1975). On some central problems in computational complexity, Doctoral Thesis. Dept. of Computer Science, Cornell University: Ithaca, NY.

  Google Scholar 

• Simovici, D. A. & Tenney, R. L. (1999). Theory of Formal Languages with Applications. World Scientific: Singapore.

  Google Scholar 

• Tanaka, Y. (1991). A Dual Algorithm for the Satis ability Problem. Information Processing Letters 37: 85–89.

  Google Scholar 

• Trakhtenbrot, B. A. (1984). A Survey of Russian Approaches to Perebor (brute-force search)algorithms. Annals of the History of Computing 6(4): 384–400.

  Google Scholar 

• Valiant, L. G. (1979). The Complexity of Enumeration and Reliability Problems. SIAM Journal on Computing 8: 410–421.

  Google Scholar 

• Valiant, L. G. (1979). The Complexity of Computing the Permanent. Theoretical Computer Science 8: 189–201.

  Google Scholar 

• Vlada, M. (1998). An Efficient Algorithm for Testing Propositional Formulas. Computers and Artificial Intelligence 17(4): 383–391.

  Google Scholar 

• Vlada, M. (2001). Algorithms for Testing Satis ability Formulas. Artificial Intelligence Review 15: 153–163.

  Google Scholar 

• Zhang, W. (1996). Number of Models and Satis ability of Sets of Clauses. Theoretical Computer Science 155: 277–288.

  Google Scholar 

Download references