In SMT/SAT solving, is there some technique to determine irrelevant variables from a formula? i.e., those that can have any value and do not not affect the satisfiability of the formula.
1 Answers
2
votes
For the case of propositional satisfiablity where a formula is a conjunction of clauses, each of which is a disjunction of literals. e.g. (A | B) & (!B | A) & (!A | B | A)
If a variable appears either only as a positive literal or only as a negative literal throughout the formula, it can be safely removed and any clauses that it appears in can be removed and regarded as satisfied. In a strict sense though, such a variable's value is not irrelevant as it may be the only variable that can satisfy those clauses in a satisfying assignment for certain formulae. Such variables are called pure and this phase is called pure literal elimination.
Before pure literal elimination, the formula should be cleaned so that any clause that contains a variable that appears both un-negated and negated is removed. This can lead to some variables becoming pure. Moreover, throughout the solution procedure, when a variable is identified as being pure, it should be eliminated.
e.g. the clause (!A | B | A) is trivially satisfied: no matter what value A takes, it is satisfied.
Then (A | B) & (!B | A) & (!A | B | A) -> (A | B) & (!B | A)
Now A is pure and can be set to True resulting in a satisfying assignment being found. Note that the solution was found without having to make any decisions, we simply applied two rules.
