An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic