I'm relatively new to the fields of formal semantics/systems/languages or even model theory and therefore I miss some knowledge and experience. I try to boil the question down to the core essence of my problem.

I've created a language $\mathcal{L}$ for feature models, a acyclic directed tree structure with additional cross-tree constraints, including a formal semantics. Part of it is the set $N$ (combined terminals and non-terminals), and the set of terminals $P \subseteq N$. $\mathcal{L}$ is finite, as the elements of $N$ can only be used a certain amount of times (ist a graph after all). Additionally, there exists a semantic evaluation function: $$[[.]]_{\mathcal{L}} : \mathcal{L} \rightarrow \mathcal{P}(\mathcal{P}(P))$$

Obviously, $|\mathcal{P}(\mathcal{P}(P))| = 2^{(2^n)}$. And I know that $\mathcal{L}$ is not expressive complete. So there exists a $p \in \mathcal{P}(\mathcal{P}(P))$ such that $$\forall d \in \mathcal{L}: [[d]]_{\mathcal{L}}\not = p$$

Now I would like to efficently check if $p$ can be expressed.

To give ourselves more opportunities, we can transform this problem to the more understood calculus of propositional formulas:


Left the informal meaning and right the semantics. Features are equivalent to propositions. A feature is either only optional or mandatory or in an alternative-group or in an or-group (only one of them!). If a feature has no sub-features it must be a terminal node (from $P$). requires/excludes are only allowed between nodes from $P$ as well.

Now, when we specify $P$ and $N$, we get a bunch of premises (all valid combinations to the semantics above,... actually quite a lot).

$p \in \mathcal{P}(\mathcal{P}(P))$ can be encoded as DNF. For example, $P = \{A,B,C\}$ and $p = \{\{A\}, \{B,C\}\}$, then $$DNF(p) = (A \wedge \neg B \wedge \neg C) \vee (\neg A \wedge B \wedge C)$$ A valid model would be $$r \wedge (NT \vee A \Leftrightarrow r) \wedge \neg (NT \wedge A) \wedge (B \Leftrightarrow NT) \wedge (C \Leftrightarrow NT) $$ with $N = \{r, NT\} \cup P$.

The problem now is the following:

Given the set of variables $P$, the set of all premises $Q = \{q_1,...,q_n\}$ over $P$ and $p \in \mathcal{P}(\mathcal{P}(P))$. $N$ is simply $\{r\} \cup P$ plus $|P|$ additional variables (each terminal-feature needs at maximum one non-terminal feature). Variables of $N$ can but don't need to be used. Can I find a subset $Q' \subseteq Q$ that is valid according to the semantics described above such that $$Q' \models DNF(p)$$ where $\models$ is the Logical consequence? Does such a subset exists?

Because $\mathcal{L}$ is finite, brute force would work. But that is not really feasable.

Final example: Given $P = \{A,B,C\}$. $p = \{\{A, B\},\{B\},\{A, C\},\{B, C\},\{A, B, C\}\}$ can't be expressed.

I would love to get some hints on what I should consider when trying to solve (or better analyse) this problem. Any direction here would be greatly appreciated.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.