When using MiniSat as C++ library, every new variable can be created as either a decision var or a non-decision var.
My rough understanding of this is that when the solver decides on which variable to use next during branching, non-decision vars are not considered. However, in my project, I ran into trouble when non-decision vars were on the left side of implication, instead of being in an equivalence relationship, as the solver returned SAT, even though the formula was actually UNSAT.
Further experimentation shows, that this only happens when the non-decision vars are in a formula that is longer than 2 variables (I guess 2-variable-formula path is a special cased in the solver, so it behaves differently).
Non-decision variables can only have their values set via inference. The only method of inference Minisat uses is the unit rule. So if setting all the decision variables doesn't cause the unit rule to be invoked to set all the non-decision variables, then the latter variables will be never be set.
The usual reason to have non-decision variables is that you know that the CNF instance is structured such that setting a fixed set of decision variables will imply values for all the other variables.
An example of this is a CNF instance to find the prime factors of some n-bit integer. The instance will necessarily implement a chain of shift-adder circuits that implement multiplication, but you only need ever set the 2(n-1) bits that are inputs to the multiplication circuit. The variables representing those bits will be the decision variables and all the other variables can be safely declared as non-decision variables.