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

Question

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

• A, B, C, and D are 4 features.
• B is a mandatory sub-feature of A
• C and D are two optional sub-features of A.

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
...

Answer 1

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?