Common variables can be detected in the same way as dead variables:
By repeated SAT solving the problem p (containing variables v1-vn), considering an additional conjecture in each run: If p AND NOT(vx) is UNSAT then vx is common (given that p is SAT).
An additional mode could be implemented that detects and outputs a list of common variables.
Common variables can be detected in the same way as dead variables:
By repeated SAT solving the problem p (containing variables v1-vn), considering an additional conjecture in each run: If p AND NOT(vx) is UNSAT then vx is common (given that p is SAT).
An additional mode could be implemented that detects and outputs a list of common variables.