Core-guided MAXSAT algorithms dominate other methods in solving industrial MAXSAT problems. In this work, we propose a new efficient algorithm that is guided by correction sets and cores. At every iteration, the algorithm obtains a correction set or a core, which is then used to rewrite the formula using incremental and succinct transformations. We theoretically show that correction sets and cores have complementary strengths and empirically demonstrate that their combination leads to an efficient MAXSAT solver that outperforms state-of-the-art WPMS solvers on the 2014 Evaluation on industrial instances.

Abstracts of the invited talks presented at the 2013 FLAIRS conference. Talks include Robotics and Assistive Technologies: Their Emerging Role in Healthcare (Howard); Crossing the Data Science Chasm: The Perception of What Data Science Is and What It Needs to Be (Johnson); Who Are My Users and How I Can Help Them? The Quest of User-Adaptive Interaction (Conati); Neural Networks in Satellite-Based Atmospheric Remote Sensing (Chen); and The Use of Automated Reasoning for Software Verification of Microsoft Products (Bjorner).