Reducing SAT to Max2SAT
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence. Main Track. Pages 1367-1373.
https://doi.org/10.24963/ijcai.2021/189
Keywords
- Constraints and SAT: MaxSAT, MinSAT
- Constraints and SAT: Constraint Optimization
- Constraints and SAT: SAT: Solvers and Applications
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.
@inproceedings{ijcai2021p189,
title = {Reducing SAT to Max2SAT},
author = {Ansótegui, Carlos and Levy, Jordi},
booktitle = {Proceedings of the Thirtieth International Joint Conference on
Artificial Intelligence, {IJCAI-21}},
publisher = {International Joint Conferences on Artificial Intelligence Organization},
editor = {Prof. Zhi-Hua Zhou},
pages = {1367--1373},
year = {2021},
month = {8},
note = {Main Track},
doi = {10.24963/ijcai.2021/189},
url = {https://doi.org/10.24963/ijcai.2021/189},
}
TY - CPAPER TI - Reducing SAT to Max2SAT AU - Ansótegui, Carlos AU - Levy, Jordi T2 - Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI-21 PB - International Joint Conferences on Artificial Intelligence Organization PY - 2021 SP - 1367 EP - 1373 DO - 10.24963/ijcai.2021/189 UR - https://doi.org/10.24963/ijcai.2021/189 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
