cnfsoftware-product-lines

How to design the CNF file from a given feature model?


I met a problem in designing the CNF (conjunctive normal form) file from a given feature model. For example, there is a general feature model in SPL.

   A
 / | \
B  C  D

How can I write the CNF file of above constraints? Any help is appreciated!

Maybe the CNF file looks like the following form,

c 1 A
c 2 B
c 3 C
c 4 D
p cnf 4 X
...

Solution

  • Your proposed format already looks similar to the DIMACS format. In this format the file contains a line for each clause of the CNF.

    To my knowledge in dimacs format your model would look like this (the // ... are not part of the clauses or the dimacs format, but rather are there for clearification):

    ... // your lines go here
    -1 2 0 // A implies B
    -2 1 0 // B implies A
    -3 1 0 // C implies A
    -4 1 0 // D implies A
    

    The trailing 0 serves as end of line or end of clause. The first two lines translates from A ↔ B. Since it is the same as A → B ^ B → A You can check Wikipedia on how the semantics of a feature model translate into logical formulas.

    Also there are several tools to create a cnf out of a given feature model. For instance FeatureIDE lets you create a feature model via a GUI and later you are able to export it in dimacs format. This format enables you to use several other tools such as SAT4J to work with your model.

    EDIT: I wonder what you mean exactly by SPL?