Simplex Implementation in z3

Question

It is mentioned here that z3 uses Dual Simplex not Revised Simplex, which would mean that as of now, all rows and columns of the original (fixed) tableaux get accessed during every pivoting operation. Am I then correct to infer that implementing Revised Simplex in z3 would substantially improve performance for problems where the tableaux happens to be large?

Answer 1

Z3's implementation of Simplex uses Dual simplex and was tuned towards backtracking search in conjunction within a DPLL(T) framework. Other approaches include the specialized solvers for difference logic, unit-two variable per inequality logic, trying revised simplex (within DPLL(T) as you suggest or some other approach) or procedures of the kind: "Dejan Jovanovic, Leonardo Mendonça de Moura: Cutting to the Chase - Solving Linear Integer Arithmetic. J. Autom. Reasoning 51(1): 79-108 (2013)", gradient methods, interior point methods, etc. There are many factors that play into what works more efficiently given an application area depending on the branching ratio vs. number of variables and inequalities in a problem.