On Solving the Partial MAX-SAT Problem

By Zhaohui Fu, Sharad Malik. International Conference on Theory and Applications of Satisfiability Testing, 2006

314 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Industrial and Manufacturing Engineering

View Paper: https://www.semanticscholar.org/paper/88fb1e37582c8cb273c5eab76caddc6bf693b54a

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 Industrial and Manufacturing Engineering

Citations in the corpus

Solving MAXSAT by Decoupling Optimization and Satisfaction (2014, methodology): “Later improvements aimed for an encoding that was mostly independent of the bound k, in order to allow more learnt clauses to be saved from one iteration to the next (Fu and Malik, 2006).”
Maximum Satisfiability Using Core-Guided MaxSAT Resolution (2014, methodology): “In this section, we discuss how our algorithm relates to the original core-based algorithm, PM1, by Fu and Malik (Fu and Malik 2006).”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, methodology): “Binary Search [47] (See Algorithm 5) maintains both a lower bound λ and an upper bound μ.”
PySAT: A Python Toolkit for Prototyping with SAT Oracles (2018, methodology): “In order to confirm this claim in practice, we developed a simple (non-optimized) PySAT-based implementation of the Fu&Malik algorithm [15] for MaxSAT.”
Open-WBO: A Modular MaxSAT Solver, (2014, methodology): “The unsatisfiability-based algorithm is based on the iterated use of a SAT solver to identify unsatisfiable subformulas [13,3,23].”
Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (2013, methodology): “It is now the state of the art to rely on this new paradigm in many applications, like in bounded model checking [7], extraction of a Minimal Unsatisfiable Set (MUS) [8], Maximum Satisfiability (MaxSAT) [9] or even inductive verification [10].”
RC2: an Efficient MaxSAT Solver (2019, background): “BLO and stratiﬁcation are known to be crucial for MaxSAT algorithms that split soft clauses of the formula involved in an unsatisﬁable core, e.g. in FM [9] and its improvements [16, 15, 3, 12], as well as OLL and RC2 [19] (also detailed above).”
Solving MAXSAT by Solving a Sequence of Simpler SAT Instances (2011, methodology): “The main prior works utilizing a sequence of SAT tests to solve Maxsat began with the work of Fu and Malik [6], and include SAT4J [4], WPM1, PM2, and WPM2 [1,2], and Msuncore [12].”
Techniques Inspired by Local Search for Incomplete MaxSAT and the Linear Algorithm: Varying Resolution and Solution-Guided Search (2019, background): “Core-guided approaches [13] repeatedly compute an unsatisﬁable core , which is a subset of clauses that cannot simultaneously be satisﬁed, and then relax the formula by allowing at most one of the clauses from the core to be unsatis-ﬁed.”
DirectFix: Looking for Simple Program Repairs (2015, methodology): “[20] Z. Fu and S. Malik, On solving the partial max-sat problem, in SAT, 2006, pp. 252 265.”