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.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.