Prolog MiniZinc equisatisfiable Gurobi Kleene Booleanization MiniSearch MicroZinc OpenWBO unsatisfiable undefinedness Choco DPLL MiniSAT Kissat AMPL subtours Zemlin makespan simpagation memoization FlatZinc Gecode CPLEX antitone QCP-max Booleanized unsatisfiability Jip Uppsala Radboud NanoZinc Ackermann nullary GBAC RCPSP Reifications SCIP QCP-Max SICStus Lille