The translation of feature models to propositional logics enabled the use of efficient reasoning systems, such as SAT solvers and BDD engines, for configuration, analysis and transformation. However, the use of such systems requires a careful examination of space and time trade-offs that these systems follow and the trade-offs that arise in the application's domain of interest. In particular, the size of a BDD structure is highly sensitive to the variable ordering chosen. Unfortunately, finding an optimal order is NP-hard, and has for long been addressed by using heuristics. In my research I investigate alternatives to enable the efficient use of logic-based reasoning in configuration by exploring specific properties of the feature modeling domain. In the following, you find information on the project including tool support and experiments. Please, feel free to contact me at [marcilio at csg dot uwaterloo dot ca].
Online Flash Demo: Click Here (press F11 to enable full-screen in your browser)
Screenshots: Click Here
· Translation of feature models to circuits and CNF
· Support for BDD- and CSP-based analysis of feature models
· Support for a specific reasoning technique called FTRA
· Support for new heuristics for BDD variable ordering
· Graphical views for:
· and more...
Tests for Binary Decision Diagrams
Feature Model Samples
Marcilio Mendonca, March, 2008.