  Satisfiability Modulo Theories (SMT) solvers check the satisfiability of
quantifier-free first-order logic formulas. We consider the theory of
non-linear real arithmetic where the formulae are logical combinations of
polynomial constraints. Here a commonly used tool is the Cylindrical Algebraic
Decomposition (CAD) to decompose real space into cells where the constraints
are truth-invariant through the use of projection polynomials.
  An improved approach is to repackage the CAD theory into a search-based
algorithm: one that guesses sample points to satisfy the formula, and
generalizes guesses that conflict constraints to cylindrical cells around
samples which are avoided in the continuing search. Such an approach can lead
to a satisfying assignment more quickly, or conclude unsatisfiability with
fewer cells. A notable example of this approach is Jovanovi\'c and de Moura's
NLSAT algorithm. Since these cells are produced locally to a sample we might
need fewer projection polynomials than the traditional CAD projection. The
original NLSAT algorithm reduced the set a little; while Brown's single cell
construction reduced it much further still. However, the shape and size of the
cell produced depends on the order in which the polynomials are considered.
  This paper proposes a method to construct such cells levelwise, i.e. built
level-by-level according to a variable ordering. We still use a reduced number
of projection polynomials, but can now consider a variety of different
reductions and use heuristics to select the projection polynomials in order to
optimise the shape of the cell under construction. We formulate all the
necessary theory as a proof system: while not a common presentation for work in
this field, it allows an elegant decoupling of heuristics from the algorithm
and its proof of correctness.
