Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/04/23 10:40] vkuncak |
sav08:small_solutions_for_quantifier-free_presburger_arithmetic [2009/09/24 15:23] vkuncak |
||
---|---|---|---|
Line 87: | Line 87: | ||
But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming. | But other solvers use solutions over rational numbers to help find solutions over integers, using techniques from integer linear programming. | ||
* {{projects:simplexdplltreport.pdf|Integrating Simplex with DPLL(T)}} | * {{projects:simplexdplltreport.pdf|Integrating Simplex with DPLL(T)}} | ||
+ | |||
+ | ===== Extensions ===== | ||
+ | |||
+ | Models get bigger if we allow bitvector operations: | ||
+ | * {{sav08:pa_bitvectors.pdf|PABitvectors}} |