March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver This paper discusses several techniques to make the look-ahead architecture for satisfiability (Sat) solvers more competitive. Our contribution consists of reduction of the computational costs to perform look-ahead and a cheap integration of both equivalence reasoning and local learning. Most proposed techniques are illustrated with experimental results of their implementation in our solver march_eq.