From Non-Clausal to Clausal MinSAT
Chu-Min Li, Felip Manyà, Joan Ramon Soler, Amanda Vidal · Frontiers in artificial intelligence and applications · 2021
We tackle the problem of solving MinSAT for multisets of propositional formulas that are not necessarily in clausal form. Our approach reduces non-clausal to clausal MinSAT, since this allows us to rely on the much developed clause-based MinSAT solvers. The main contribution of this paper is the definition of several transformations of multisets of propositional formulas into multisets of clauses so that the maximum number of unsatisfied clauses in both multisets is preserved.