Combining Satisfiability Procedures Combining satisfiability procedures is non trivial And that is to be expected: Equality was solved by Ackerman in 1924,arithmetic by Fourier even before,but E+A only in 1979 yet in any single verification problem we will have literals from several theories: Equality,arithmetic,lists,... When and how can we combine separate satisfiability procedures? Prof.Necula CS 294-8 Lecture 12 5Prof. Necula CS 294-8 Lecture 12 5 Combining Satisfiability Procedures • Combining satisfiability procedures is non trivial • And that is to be expected: – Equality was solved by Ackerman in 1924, arithmetic by Fourier even before, but E + A only in 1979 ! • Yet in any single verification problem we will have literals from several theories: – Equality, arithmetic, lists, … • When and how can we combine separate satisfiability procedures?