Skip to main content
SpringerLink
Log in

Propositional calculus problems in CHIP

  • Conference paper
  • First Online:
Book cover Algebraic and Logic Programming (ALP 1990)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 463))

Included in the following conference series:

Abstract

This paper describes how to model and solve boolean satisfiability problems with the constraint logic programming language CHIP. Although CHIP has not been developed as a specialised propositional calculus prover, it can solve these problems quite efficiently. Several different methods of describing satisfiability problems in CHIP are presented and compared. This flexibility of modelling is a major advantage of CHIP over closed problem solvers. We have evaluated various sets of benchmarks taken from [31] [16] [21]. With one exception, CHIP performs as well or better as specialised programs on these examples. We also shortly discuss an alternative modeling technique using finite domain variables not restricted to 0/1 values.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. W. Buettner and H. Simonis. Embedding Boolean Expressions into Logic Programming. Journal of Symbolic Computation, 4:191–205, October 1987.

    Google Scholar 

  2. L. Claesen. Proceedings IFIP WG 10.2 WG 10.5 International Workshop on Applied Formal Methods for Correct VLSI Design. Elsevier Science Publishers, Leuven, Belgium, November 1989.

    Google Scholar 

  3. G.B. Dantzig. Linear Programming and Extensions. Princeton University Press, Princeton, New Jersey, 1963.

    Google Scholar 

  4. M. Davis and H. Putnam. A computing procedure for quantification theory. JACM, 7:201–215, 1960.

    Google Scholar 

  5. M. Dincbas, H. Simonis, and P. Van Hentenryck. Extending Equation Solving and Constraint Handling in Logic Programming. In Proceedings of Colloquium on the Resolution of Equations in Algebraic Structures (CREAS), Austin, Texas, USA, May 1987. MCC.

    Google Scholar 

  6. M. Dincbas, H. Simonis, and P. Van Hentenryck. Solving Large Combinatorial Problems in Logic Programming. Journal of Logic Programming, 8(1, 2):74–94, January–March 1990.

    Google Scholar 

  7. M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, and T. Graf. Applications of CHIP to Industrial and Engineering Problems. In First International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems, Tullahoma, Tennessee, USA, June 1988.

    Google Scholar 

  8. M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, T. Graf, and F. Berthier. The Constraint Logic Programming Language CHIP. In Proceedings on the International Conference on Fifth Generation Computer Systems FGCS-88, Tokyo, Japan, December 1988.

    Google Scholar 

  9. W. Dowling and J. Gallier. Linear-Time Algorithm for Testing the Satisfiability of Propositional Horn Formulae. Journal of Logic Programming, 3:267–284, 1984.

    Google Scholar 

  10. G. Gallo and G. Urbani. Algorithms for Testing the Satisfiability of Propositional Formulae. Journal of Logic Programming, 7:45–61, 1989.

    Google Scholar 

  11. M.R. Garey and D.S. Johnson. Computers and Intractability. W.H. Freeman and Company, New York, 1979.

    Google Scholar 

  12. R. Garfinkel and G. Nemhauser. Integer Programming. John Wiley, Chichester, UK, 1972.

    Google Scholar 

  13. T. Graf. Extending Constraint Handling in Logic Programming to Rational Arithmetic. Rapport de stage, DESS-ISI, Sophia Antipolis, France, September 1987.

    Google Scholar 

  14. T. Graf. Raisonner sur les contraintes en programmation en logique. PhD thesis, Université de Nice, France, September 1989. (in French).

    Google Scholar 

  15. ISCAS. Special Session on ATPG. In Proc IEEE Symposium on Circuits and Systems, July 1985.

    Google Scholar 

  16. J-L. Lauriere. A Language and a Program for Stating and Solving Combinatorial Problems. Artificial Intelligence, 10(1):29–127, 1978.

    Google Scholar 

  17. D. Loveland. Automated Theorem Proving. North Holland, 1978.

    Google Scholar 

  18. A.K. Mackworth. Consistency in Networks of Relations. AI Journal, 8(1):99–118, 1977.

    Google Scholar 

  19. R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In Proceedings of the 9th International Conference on Automated Deduction (CADE), pages 415–434, Argonne, Ill, May 1988. Springer.

    Google Scholar 

  20. Ursula Martin and Tobias Nipkow. Boolean Unification — The Story So Far. Journal of Symbolic Computation, 7:275–293, 1989.

    Google Scholar 

  21. A. Rauzy. L'Evaluation Semantique en Calcul Propositionnel. PhD thesis, Universite Aix-Marseille II, Marseille, France, January 1989. (in French).

    Google Scholar 

  22. J. Roth. Diagnosis of Automata Failure: A Calculus and a Method. IBM Journal of Research and Development, 10:278–291, 1966.

    Google Scholar 

  23. K. Sakai and Y. Sato. Boolean Groebner Bases. Technical report, ICOT, Tokyo, Japan, June 1988.

    Google Scholar 

  24. J.H. Siekmann. Universal unification. In 7th International Conference on Automated Deduction, pages 1–42, Napa Valley, CA, 1984.

    Google Scholar 

  25. H. Simonis. Test Generation using the Constraint Logic Programming Language CHIP. In Proceedings of the 6th International Conference on Logic Programming, Lisboa, Portugal, June 1989.

    Google Scholar 

  26. H. Simonis and M. Dincbas. Using an Extended Prolog for Digital Circuit Design. In IEEE International Workshop on AI Applications to CAD Systems for Electronics, pages 165–188, Munich, W.Germany, October 1987.

    Google Scholar 

  27. H. Simonis and M. Dincbas. Using Logic Programming for Fault Diagnosis in Digital Circuits. In German Workshop on Artificial Intelligence (GWAI-87), pages 139–148, Geseke, W.Germany, September 1987.

    Google Scholar 

  28. H. Simonis and M. Dincbas. Solving Propositional Calculus Problems in CHIP. Technical Report TR-LP-46, E.C.R.C. (European Computer-Industry Research Centre), May 1990.

    Google Scholar 

  29. H. Simonis and T. Le Provost. Circuit Verification in CHIP: Benchmark Results. In L.J.M. Claesen, editor, Proceedings of the IFIP TC10/WG10.2/WG10.5 Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Belgium, November 1989. IFIP, North Holland, Elsevier Science Publishers.

    Google Scholar 

  30. G.J. Sussman and G.L. Steele. CONSTRAINTS-A Language for Expressing Almost-Hierarchical Descriptions. AI Journal, 14(1), 1980.

    Google Scholar 

  31. K. Truemper and F.J. Radermacher. Analyse der Leistungsfaehigkeit eines neuen Systems zur Auswertung aussagenlogischer Probleme. Technical Report FAW-TR-90003, FAW, Ulm, FRG, February 1990. (in German).

    Google Scholar 

  32. P. Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic Programming Series. MIT Press, Cambridge, Ma, 1989.

    Google Scholar 

  33. L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning. Prentice Hall, Englewood Cliffs, New Jersey, 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. European Computer-Industry Research Centre GmbH, Arabellastr. 17, D-8000, München 81, Germany

    H. Simonis & M. Dincbas

Authors
  1. H. Simonis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. Dincbas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hélène Kirchner Wolfgang Wechler

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Simonis, H., Dincbas, M. (1990). Propositional calculus problems in CHIP. In: Kirchner, H., Wechler, W. (eds) Algebraic and Logic Programming. ALP 1990. Lecture Notes in Computer Science, vol 463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53162-9_39

Download citation

  • DOI: https://doi.org/10.1007/3-540-53162-9_39

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-53162-3

  • Online ISBN: 978-3-540-46738-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation