A Declarative Encoding of Telecommunications Feature Subscription in SAT
Proceedings of the 11th International ACM SIGPLAN Conference
on Principles and Practice of Declarative Programming (PPDP 2009);
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.
Related sites: random data instances from CP08 paper
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel