Beyond Core-Guided MaxSAT
A new proof system for MaxSAT is described, the Comparator Calculus, which models the inferential strategies used in core-guided MaxSAT solvers and two new MaxSAT algorithms are introduced: a core-guided one (CSimple) and one non-core-guided (CSat), which uses heuristics to construct new soft formulas and calls a SAT s...