---
title: "Reducing SAT to Max2SAT"
authors:
  - "Carlos Ansótegui"
  - "Jordi Levy"
doi: "10.24963/ijcai.2021/189"
url: "https://ijcai.org/proceedings/2021/189"
pdf: "https://ijcai.org/proceedings/2021/0189.pdf"
venue: "Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence"
year: 2021
pages: "1367-1373"
track: "Main Track"
keywords:
  - "Constraints and SAT: MaxSAT, MinSAT"
  - "Constraints and SAT: Constraint Optimization"
  - "Constraints and SAT: SAT: Solvers and Applications"
---

# Reducing SAT to Max2SAT

Carlos Ansótegui, Jordi Levy

*Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence*, pages 1367-1373. DOI: [10.24963/ijcai.2021/189](https://doi.org/10.24963/ijcai.2021/189)

## 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.