Search
 
loader loading subjects...
cover
From Non-Clausal to Clausal MinSAT
Chu-Min Li, Felip Manyà, Joan Ramon Soler, Amanda Vidal
27 - 36
10.3233/FAIA210113
Research Article
Frontiers in Artificial Intelligence and Applications
Volume 339: Artificial Intelligence Research and Development
Abstract

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.

Download
Creative Commons License