reading chapter 11 “Conflict Analysis” of “Constraint Integer Programming” (by Tobias Achterberg), which introduces SAT-like conflict analysis and non-chronological backtracks into LP-based branch-and-bound MIP solver.