Compiling Problem Specifications into SAT

  • Marco Cadoli1
  • Andrea Schaerf
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


We present a compiler that translates a problem specification into a propositional satisfiability test (SAT). Problems are specified in a logic-based language, called np-spec, which allows the definition of complex problems in a highly declarative way, and whose expressive power is such to capture exactly all problems which belong to the complexity class NP. The target SAT instance is solved using any of the various state- of-the-art solvers available from the community. The system obtained is an executable specification language for all NP problems which shows interesting computational properties. The performances of the system have been tested on a few classical problems, namely graph coloring, Hamiltonian cycle, and job-shop scheduling.


Hamiltonian Cycle Graph Coloring Hamiltonian Path Conjunctive Normal Form Predicate Symbol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    A. Aggoun et al. ECL i PS e User Manual (Version 4.0). IC-Parc, London (UK), July 1998.Google Scholar
  2. 2.
    K. R. Apt, H. A. Blair, and A. Walker. Towards a theory of declarative knowledge. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 89–142. Morgan Kaufmann, Los Altos, 1988.Google Scholar
  3. 3.
    M. Cadoli, G. Ianni, L. Palopoli, A. Schaerf, and D. Vasile. np-spec: An executable specification language for solving all problems in NP. Technical Report 00-13, Dip. di Inf. e Sist., Univ. di Roma “La Sapienza”, 2000.Google Scholar
  4. 4.
    M. Cadoli and L. Palopoli. Circumscribing datalog: expressive power and complexity. Theor. Comp. Sci., 193:215–244, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    M. Cadoli, L. Palopoli, A. Schaerf, and D. Vasile. np-spec: An executable specification language for solving all problems in NP. In Proc. of PADL’99, number 1551 in LNAI, pages 16–30. Springer-Verlag, 1999.Google Scholar
  6. 6.
    P. Cheeseman, B. Kanefski, and W. M. Taylor. Where the really hard problem are. In Proc. of IJCAI’91, pages 163–169, 1991.Google Scholar
  7. 7.
    J. M. Crawford and A. B. Baker. Experimental results on the application of satisfiability algorithms to scheduling problems. In Proc. of AAAI’94, pages 1092–1097, 1994.Google Scholar
  8. 8.
    M. Davis, G. Logemann, and D. W. Loveland. A machine program for theorem proving. Comm. of the ACM, 5(7):394–397, 1962.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    M. Davis and H. Putnam. A computing procedure for quantification theory. J. of the ACM, 7:201–215, 1960.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    T. Eiter, N. Leone, C. Mateis, G. Pfeifer, and F. Scarcello. The KR system dlv: Progress report, Comparisons and Benchmarks. In Proc. of KR’98, pages 406–417, 1998.Google Scholar
  11. 11.
    M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proc. of IJCAI’93, pages 52–57, 1993.Google Scholar
  12. 12.
    M. R. Garey and D. S. Johnson. Computers and Intractability―A guide to NP-completeness. W.H. Freeman and Company, San Francisco, 1979.zbMATHGoogle Scholar
  13. 13.
    D. Jackson. Automating first-order relational logic. In Proc. of ACM SIGSOFT’00: 8th SIGSOFT Symposium on Foundation of Software Engineering, 2000.Google Scholar
  14. 14.
    D. S. Johnson, C. R. Aragon, L. A. McGeoch, and C. Schevon. Optimization by simulated annealing: an experimental evaluation; part II, graph coloring and number partitioning. Operations Research, 39(3):378–406, 1991.zbMATHCrossRefGoogle Scholar
  15. 15.
    D. S. Johnson and M. A. Trick, eds. Cliques, Coloring, and Satisfiability. Second DIMACS Implementation Challenge, volume 26 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science. American Math. Soc., 1996.Google Scholar
  16. 16.
    H. A. Kautz, D. McAllester, and B. Selman. Encoding plans in propositional logic. In Proc. of KR’96, pages 374–384, 1996.Google Scholar
  17. 17.
    H. A. Kautz and B. Selman. Planning as satisfiability. In Proc. of ECAI’92, pages 359–363, 1992.Google Scholar
  18. 18.
    T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Trans. on Computer-Aided Design, pages 4–15, 1992.Google Scholar
  19. 19.
    C. Li and Anbulagan. Heuristics based on unit propagation for satisfiability pro blems. In Proc. of IJCAI’97, pages 366–371, 1997.Google Scholar
  20. 20.
    V. Lifschitz. Computing circumscription. In Proc. of IJCAI’85, pages 121–127, 1985.Google Scholar
  21. 21.
    F. Massacci and L. Marraro. Logical cryptanalysis as a SAT-problem: Encoding and analysis of the U.S. Data Encryption Standard. J. of Automated Reasoning, 24(1-2):165–203, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    I. Niemelä. Logic programs with stable model semantics as a constraint programming paradigm. Ann. of Mathematics and Artif. Intell., 25(3,4):241–273, 1999.Google Scholar
  23. 23.
    SATLIB-The Satisfiability Library.
  24. 24.
    B. Selman, H. Kautz, and B. Cohen. Noise strategies for improving local search. In Proc. of AAAI’94, pages 337–343, 1994.Google Scholar
  25. 25.
    B. Selman, D. Mitchell, and H. Levesque. Generating Hard Satisfiability Problems. Artificial Intelligence, 81:17–29, 1996.CrossRefMathSciNetGoogle Scholar
  26. 26.
    M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. J. of the ACM, 23(4):733–742, 1976.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Marco Cadoli1
    • 1
  • Andrea Schaerf
    • 2
  1. 1.Dipartimento di Informatica e SistemisticaUniversità di Roma “La Sapienza”RomaItaly
  2. 2.Dipartimento di Ingegneria Elettrica, Gestionale e MeccanicaUniversità di UdineUdineItaly

Personalised recommendations