Farkas-Based Tree Interpolation

on YouTube ↗19m

" summary

Paper studies Farkas-lemma based interpolation for quantifier-free linear real arithmetic (SMT) and classifies five algorithms by whether they guarantee tree interpolation. Main claims: Farkas interpolants satisfy TIP, dual and flexible variants do not, and the decomposed Farkas approach guarantees TIP under a monotonicity constraint enforced by gradual decomposition. Evaluation on benchmarks shows decomposed interpolants have more top-level conjuncts on 91% of cases and plain Farkas interpolants have fewer unique LRA atoms on 63%. An application called UpProver is implemented.

AI-written summary · about

" chapters (18)

1. 0:00Intro
2. 0:20From Binary to Tree Interpolants
3. 1:40Example
4. 2:23Craig/Binary Interpolants
5. 3:00Dual Interpolants
6. 3:21Tree Interpolation Property (TIP)
7. 4:30Why tree interpolation property is required?
8. 6:30Outline (Contributions) Overview on existing binary interpolation algorithms in LRA
9. 7:22Farkas coefficients
10. 8:28Dual Farkas Interpolant
11. 10:36Combining LRA & Propositional is tricky ... (cont'd)
12. 12:40Solution: Proper Labeling to determine the partitioning of theory clauses
13. 13:08TIP in Farkas Algorithm (Proof by Induction)
14. 13:54Outline (Open Issues and Contributions) Overview on different binary interpolation algorithms in LRA 1 FARKAS
15. 14:09Constraints on decompositions to guarantee TIP Monotonicity Condition: The inequalities resulting from supersystem's decomposition must be logically covered by the inequalities of subsystem's decomposition
16. 14:30Gradual Decomposition
17. 17:00Experiments: Farkas (1 ) vs. Decomposed Farkas (1) tree interpolants Benchmarks: 514 QF_LRA UNSAT formulas, up to 12k Loc
18. 18:07Related Work