Resolution search

AbstractBranch-and-bound is one of the most popular ways of solving difficult problems such as integer and mixed-integer linear programming problems; when the branching is done on zero-one valued variables, the resulting variant of branch-and-bound is called implicit enumeration. Efficiency of branch-and-bound and implicit enumeration algorithms depends heavily on the branching strategy used to select the next variable to branch on and its value. We propose an alternative to implicit enumeration. Our algorithm, which we call resolution search, seems to suffer less from inappropriate branching strategies than implicit enumeration does