An Exact Inference Scheme for MinSAT
Abstract
We describe an exact inference-based algorithm for the MinSAT problem. Given a multiset of clauses Φ, the algorithm derives as many empty clauses as the maximum number of clauses that can be falsified in Φ by applying finitely many times an inference rule, and returns an optimal assignment. We prove the correctness of the algorithm, describe how it can be extended to deal with weighted MinSAT and weighted partial MinSAT instances, analyze the differences between the MaxSAT and MinSAT inference schemes, and define and empirically evaluate the MinSAT Pure Literal Rule.
Cite
Text
Li and Manyà. "An Exact Inference Scheme for MinSAT." International Joint Conference on Artificial Intelligence, 2015.Markdown
[Li and Manyà. "An Exact Inference Scheme for MinSAT." International Joint Conference on Artificial Intelligence, 2015.](https://mlanthology.org/ijcai/2015/li2015ijcai-exact/)BibTeX
@inproceedings{li2015ijcai-exact,
title = {{An Exact Inference Scheme for MinSAT}},
author = {Li, Chu Min and Manyà, Felip},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2015},
pages = {1959-1965},
url = {https://mlanthology.org/ijcai/2015/li2015ijcai-exact/}
}