Local Search Algorithms for Partial MAXSAT

Abstract

MAXSAT solutions, i.e., near-satisfying assignments for propositional formulas, are sometimes meaningless for real-world problems because such formulas include "mandatory clauses" that must be all satisfied for the solution to be reasonable. In this paper, we introduce Partial MAXSAT and investigate how to solve it using local search algorithms. An instance of Partial MAXSAT consists of two formulas fA and fB , and its solution must satisfy all clauses in fA and as many clauses in f B as possible. The basic idea of our algorithm is to give weight to fA --clauses (the mandatory clauses) and then apply local search. We face two problems; (i) what amount of weight is appropriate and (ii) how to deal with the common action of local search algorithms, giving weight to clauses for their own purpose, which will hide the initial weight as the algorithms proceed. Introduction Local search has already become an important paradigm for solving propositional CNF satisfiability. Since it was shown...

Cite

Text

Cha et al. "Local Search Algorithms for Partial MAXSAT." AAAI Conference on Artificial Intelligence, 1997.

Markdown

[Cha et al. "Local Search Algorithms for Partial MAXSAT." AAAI Conference on Artificial Intelligence, 1997.](https://mlanthology.org/aaai/1997/cha1997aaai-local/)

BibTeX

@inproceedings{cha1997aaai-local,
  title     = {{Local Search Algorithms for Partial MAXSAT}},
  author    = {Cha, Byungki and Iwama, Kazuo and Kambayashi, Yahiko and Miyazaki, Shuichi},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {1997},
  pages     = {263-268},
  url       = {https://mlanthology.org/aaai/1997/cha1997aaai-local/}
}