Reducing SAT to Max2SAT
Abstract
In the literature, we find reductions from 3SAT to Max2SAT. These reductions are based on the usage of a gadget, i.e., a combinatorial structure that allows translating constraints of one problem to constraints of another. Unfortunately, the generation of these gadgets lacks an intuitive or efficient method. In this paper, we provide an efficient and constructive method for Reducing SAT to Max2SAT and show empirical results of how MaxSAT solvers are more efficient than SAT solvers solving the translation of hard formulas for Resolution.
Cite
Text
Ansótegui and Levy. "Reducing SAT to Max2SAT." International Joint Conference on Artificial Intelligence, 2021. doi:10.24963/IJCAI.2021/189Markdown
[Ansótegui and Levy. "Reducing SAT to Max2SAT." International Joint Conference on Artificial Intelligence, 2021.](https://mlanthology.org/ijcai/2021/ansotegui2021ijcai-reducing/) doi:10.24963/IJCAI.2021/189BibTeX
@inproceedings{ansotegui2021ijcai-reducing,
title = {{Reducing SAT to Max2SAT}},
author = {Ansótegui, Carlos and Levy, Jordi},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2021},
pages = {1367-1373},
doi = {10.24963/IJCAI.2021/189},
url = {https://mlanthology.org/ijcai/2021/ansotegui2021ijcai-reducing/}
}