A declarative encoding of telecommunications feature subscription in SAT

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A declarative encoding of telecommunications feature subscription in SAT

Full text

Pdf (551 KB)

Source

International Conference on Principles and Practice of Declarative Programming archive
Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming table of contents

Coimbra, Portugal

SESSION: Constraints table of contents

Pages 255-266

Year of Publication: 2009

ISBN:978-1-60558-568-0

Authors

Michael Codish	Ben-Gurion University of the Negev, Beer-Sheva, Israel
Samir Genaim	Universidad Complutense de Madrid, Madrid, Spain
Peter J. Stuckey	University of Melbourne, Australia, Melbourne, Australia

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 5, Citation Count: 0

Additional Information:

abstract references index terms

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1599410.1599442 What is a DOI?

ABSTRACT

This paper describes the encoding of a telecommunications feature subscription configuration problem to propositional logic and its solution using a state-of-the-art Boolean satisfaction solver. The transformation of a problem instance to a corresponding propositional formula in conjunctive normal form is obtained in a declarative style. An experimental evaluation indicates that our encoding is considerably faster than previous approaches based on the use of Boolean satisfaction solvers. The key to obtaining such a fast solver is the careful design of the Boolean representation and of the basic operations in the encoding. The choice of a declarative programming style makes the use of complex circuit designs relatively easy to incorporate into the encoder and to fine tune the application.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Gregory W. Bond, Eric Cheung, K. Hal Purdy, Pamela Zave, and J. Christopher Ramming. An open architecture for next-generation telecommunication services. ACM Trans. Internet Techn., 4(1):83--123, 2004.
	2	Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. Telecommunications feature subscription as a partial order constraint problem. In Maria Garcia de la Banda and Enrico Pontelli, editors, ICLP, volume 5366 of Lecture Notes in Computer Science, pages 749--753. Springer, 2008a. ISBN 978-3-540-89981-5.
	3	Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. Solving partial order constraints for LPO termination. Journal on Satisfiability, Boolean Modeling and Computation, 5:193--215, 2008b. (an earlier version appears in the proceedings of RTA 2006, LNCS 4098).
	4	Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. Logic programming with satisfiability. TPLP, 8(1):121--128, 2008c.
	5	Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to algorithms. MIT Press and McGraw-Hill, 1990.
	6	Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003 (Selected Revised Papers), volume 2919 of Lecture Notes in Computer Science, pages 502--518. Springer, 2004.
	7	Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into sat. JSAT, 2(1-4):1--26, 2006.
	8	Guy Even. On teaching fast adder designs: Revisiting ladner & fischer. In Oded Goldreich, Arnold L. Rosenberg, and Alan L. Selman, editors, Essays in Memory of Shimon Even, volume 3895 of Lecture Notes in Computer Science, pages 313--347. Springer, 2006. ISBN 3-540-32880-7.
	9	Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Hand-book of Knowledge Representation, volume 3 of Foundations of Artificial Intelligence, chapter Satisfiability Solvers, pages 89--134. Elsevier, 2008. Editors: Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter.
	10	R.M. Karp. Reducibility among Combinatorial Problems, pages 85--103. Plenum Press, 1972. R.E. Miller and J.M. Thatcher (eds.).
	11	David Lesaint, Deepak Mehta, Barry O'Sullivan, Luis O. Quesada, and Nic Wilson. Solving a telecommunications feature subscription configuration problem. In Peter J. Stuckey, editor, CP, volume 5202 of Lecture Notes in Computer Science, pages 67--81. Springer, 2008. ISBN 978-3-540-85957-4. (an earlier version appears in the Proceedings of Innovative Applications of Artificial Intelligence, July 2008).
	12	MiniSAT. MiniSAT. http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat. Viewed December 2005.
	13	Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In DAC, pages 530--535. ACM, 2001. ISBN 1-58113-297-2.
	14	Jan Wielemaker. An overview of the SWI-Prolog programming environment. In Fred Mesnard and Alexander Serebenik, editors, Proceedings of the 13th International Workshop on Logic Programming Environments, pages 1--16, Heverlee, Belgium, December 2003. Katholieke Universiteit Leuven. CW 371.
	15	Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, and Sharad Malik. Efficient conflict driven learning in a boolean satisfiability solver. In ICCAD '01: Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, pages 279--285, Piscataway, NJ, USA, 2001. IEEE Press. ISBN 0-7803-7249-2.