Superresolution and P-Optimality in Boolean MAX-CSP Solvers
Ahmed Abdelmeged, Christine Hang, Daniel Rinehart, Karl J. Lieberherr · 2007
Abstract. The maximum constraint satisfaction problem MAX-CSP is a general framework in which many search problems can be readily modeled. We integrate two lines of research from the 1970s, superresolution and P-optimal algorithms, into one MAX-CSP(Γ)-transition system SPOT. Superresolution is a non-redundant clause learning system with aggressive restarts that formalizes non-chronological backtracking. P-optimal algorithms satisfy in polynomial time a fraction τΓ of the the constraints for constraint language Γ while the fraction τΓ +ɛ is NP-complete. SPOT consists of three novel components: AR, IR and TS. We use a logarithmic abstract representation (AR) to map MAX-CSP(Γ)instances to look-ahead polynomials that provide a blurry, yet optimal view into the search space with outstanding peripheral vision. We provide a novel intermediate representation (IR) to very efficiently manipulate relations by representing them as integers. We introduce a transition system (TS) that generalizes superresolution from SAT to MAX-CSP. Superresolution counteracts the blurry vision of the look-ahead polynomials by pushing the maximum assignment into the periphery where the look-ahead polynomials see best. We discuss the implementation of SPOT and compare its behavior to zChaff and Yices with encouraging results. Our implementation uses principles of Adaptive and Aspect-Oriented Programming to provide for a solver that is easy to experiment with. 1