RC2: an Efficient MaxSAT Solver

By Alexey Ignatiev. 2019

138 citations recorded by the source corpus.

Recent work proposed a toolkit PySAT aiming at fast and easy prototyping with propositional satisfiability (SAT) oracles in Python, which enabled one to exploit the power of the original implementations of the state-of-the-art SAT solvers in Python. Maximum satisfiability (MaxSAT) is a well-known optimization version of SAT, which can be solved with a series of calls to a SAT oracle. Based on this fact and motivated by the ideas underlying the PySAT toolkit, this paper describes and evaluates RC2 (stands for relaxable cardinality constraints), a new core-guided MaxSAT solver written in Python, which won both unweighted and weighted categories of the main track of MaxSAT Evaluation 2018.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Optimal Decision Lists using SAT (2020, methodology): “Implementation All the models proposed in Section 4, and Section 5 are implemented as a set of Python scripts and solving is done by instrumenting calls to exact MaxSAT solver RC2-B (Ignatiev, Morgado, and Marques-Silva 2018, 2019).”
Computing Optimal Decision Sets with SAT (2020, methodology): “To tackle the MaxSAT models, the RC2-B MaxSAT solver was used [28].”
Learning Optimal Decision Trees with MaxSAT and its Integration in AdaBoost (2020, positive): “We use the RC2 MaxSAT solver [ Ignatiev et al. , 2019 ] .”
On Relating Explanations and Adversarial Examples (2019, methodology): “The implementation of minimum hitting set enumeration of Algorithm 1 is based on an award-winning maximum satisfiability solver RC26 [22] written on top of the PySAT toolkit [21].”