Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
A. Aggoun et al. ECL i PS e User Manual (Version 4.0). IC-Parc, London (UK), July 1998.
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.
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.
M. Cadoli and L. Palopoli. Circumscribing datalog: expressive power and complexity. Theor. Comp. Sci., 193:215–244, 1998.
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.
P. Cheeseman, B. Kanefski, and W. M. Taylor. Where the really hard problem are. In Proc. of IJCAI’91, pages 163–169, 1991.
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.
M. Davis, G. Logemann, and D. W. Loveland. A machine program for theorem proving. Comm. of the ACM, 5(7):394–397, 1962.
M. Davis and H. Putnam. A computing procedure for quantification theory. J. of the ACM, 7:201–215, 1960.
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.
M. Fujita, J. Slaney, and F. Bennett. Automatic generation of some results in finite algebra. In Proc. of IJCAI’93, pages 52–57, 1993.
M. R. Garey and D. S. Johnson. Computers and Intractability―A guide to NP-completeness. W.H. Freeman and Company, San Francisco, 1979.
D. Jackson. Automating first-order relational logic. In Proc. of ACM SIGSOFT’00: 8th SIGSOFT Symposium on Foundation of Software Engineering, 2000.
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.
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.
H. A. Kautz, D. McAllester, and B. Selman. Encoding plans in propositional logic. In Proc. of KR’96, pages 374–384, 1996.
H. A. Kautz and B. Selman. Planning as satisfiability. In Proc. of ECAI’92, pages 359–363, 1992.
T. Larrabee. Test pattern generation using Boolean satisfiability. IEEE Trans. on Computer-Aided Design, pages 4–15, 1992.
C. Li and Anbulagan. Heuristics based on unit propagation for satisfiability pro blems. In Proc. of IJCAI’97, pages 366–371, 1997.
V. Lifschitz. Computing circumscription. In Proc. of IJCAI’85, pages 121–127, 1985.
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.
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.
SATLIB-The Satisfiability Library. http://www.informatik.tu-darmstadt.de/AI/SATLIB.
B. Selman, H. Kautz, and B. Cohen. Noise strategies for improving local search. In Proc. of AAAI’94, pages 337–343, 1994.
B. Selman, D. Mitchell, and H. Levesque. Generating Hard Satisfiability Problems. Artificial Intelligence, 81:17–29, 1996.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cadoli1, M., Schaerf, A. (2001). Compiling Problem Specifications into SAT. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_26
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_26
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive