How do you come to this conclusion? They way I read it rather sounds like they use the CP-SAT solver with LNS and LS workers, parallelized over multiple machines