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:
https://en.wikipedia.org/wiki/Feature_model
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.