# Finding a common variable value among all SAT solutions

Let $$F$$ be a boolean formula on $$n$$ variables $$x_1, \cdots, x_n$$. $$\textbf{SAT}(F)$$ asks whether there exists an assignment of truth values to variables under which $$F$$ is true. I'm curious about another problem: given $$F$$, is there a variable $$x_i$$ whose truth value is the same across all truth assignments that satisfy $$F$$, if any? A couple ways to rephrase this: is there some index $$i$$ such that

• at least one of $$F \wedge x_i$$ or $$F \wedge \neg x_i$$ is unsatisfiable?
• at least one of $$F\implies x_i$$ or $$F\implies\neg x_i$$ is a tautology?
• (by completeness) at least one of $$F\implies x_i$$ or $$F\implies \neg x_i$$ has a derivation?

We could also ask for a concrete witness for $$i$$, i.e. a choice of $$F\implies x_i$$ or $$F\implies \neg x_i$$.

I have a couple questions:

1. Does this problem appear in the SAT/theorem-proving literature with a specific name that I can look for? For instance, roughly speaking, does this problem behave any nicer than the general problem of checking if a formula is a tautology?
2. In terms of computational techniques/heuristics, how far does this problem differ from SAT and its variants? I'm hoping we can do better than just querying $$\textbf{SAT}(F \wedge x_i)$$ and $$\textbf{SAT}(F \wedge \neg x_i)$$ for each index $$i$$.

My first thought was that being able to deduce "forced" variable values sounds useful for SAT solvers -- so perhaps some fast solvers have machinery to that end? But naively, it doesn't look like an easier problem than SAT; for example, an answer of no to this problem on a formula $$F$$ implies that $$F$$ has at least two models, hence an answer of yes for $$\textbf{SAT}(F)$$. To me, it feels like there might be a fundamental difference between the "exhaustive" nature of searching for a satisfying assignment and the "deductive" nature of making syntactic reductions until a consequence of the form $$x_i$$ or $$\neg x_i$$ is reached.