RC2: an Efficient MaxSAT Solver

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

Research output: Contribution to journalArticleResearchpeer-review


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.
Original languageEnglish
Pages (from-to)53-64
Number of pages12
JournalJournal on Satisfiability, Boolean Modeling and Computation
Issue number1
Publication statusPublished - 1 Sep 2019
Externally publishedYes


  • Maximum Satisability
  • Relaxable/Soft Cardinality Constraints
  • Python

Cite this