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

• Type: Conference
• Year: 2009
• Where: PPDP
• Authors: Michael Codish, Samir Genaim, Peter J. Stuckey
• Keywords: Boolean Satisfaction Solvers, Corresponding Propositional Formula, PPDP 2009, Programming Languages, State-of-the-art Boolean Satisfaction