We describe work in progress dedicated to a decision procedure for
disjunctive linear arithmetic, based on traversing in various ways the 
linear hyperplane arrangement induced by the input formula's predicates.
We propose two methods:

1. a method by which theory propagation is approximated, with the use of 
hints (clauses that only affect decisions in the SAT solver, but do not 
participate in conflicts)

2. 'reversed DPLL(T)', by which the theory leads the search rather than the SAT  solver. We show a concrete algorithm for traversing the cells in the linear  hyperplane arrangement, which can be the base for such a procedure.