Sciweavers

Share
PPDP
2009
Springer

A declarative encoding of telecommunications feature subscription in SAT

9 years 4 months ago
A declarative encoding of telecommunications feature subscription in SAT
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. Categories and Subject Descriptors D.3.2 [Programming Langauges]: Language Classifications—Constraint and logic lan
Michael Codish, Samir Genaim, Peter J. Stuckey
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where PPDP
Authors Michael Codish, Samir Genaim, Peter J. Stuckey
Comments (0)
books