Maximum Satisfiability (MaxSAT) is a well-known optimization variant of propositional Satisfiability (SAT). Motivated by a growing number of practical applications, recent years have seen the development of different MaxSAT algorithms based on iterative SAT solving. Such algorithms perform well on problem instances originating from practical applications. This paper proposes a new core-guided MaxSAT algorithm. This new algorithm builds on the recently proposed unclasp algorithm for ASP optimization problems, but focuses on reusing the encoded cardinality constraints. Moreover, the proposed algorithm also exploits recently proposed weighted optimization techniques. Experimental results obtained on industrial instances from the most recent MaxSAT evaluation, indicate that the proposed algorithm achieves increased robustness and improves overall performance, being capable of solving more instances than state-of-theart MaxSAT solvers. © 2014 Springer International Publishing Switzerland.

Core-guided MaxSAT with soft cardinality constraints

Dodaro C.;
2014

Abstract

Maximum Satisfiability (MaxSAT) is a well-known optimization variant of propositional Satisfiability (SAT). Motivated by a growing number of practical applications, recent years have seen the development of different MaxSAT algorithms based on iterative SAT solving. Such algorithms perform well on problem instances originating from practical applications. This paper proposes a new core-guided MaxSAT algorithm. This new algorithm builds on the recently proposed unclasp algorithm for ASP optimization problems, but focuses on reusing the encoded cardinality constraints. Moreover, the proposed algorithm also exploits recently proposed weighted optimization techniques. Experimental results obtained on industrial instances from the most recent MaxSAT evaluation, indicate that the proposed algorithm achieves increased robustness and improves overall performance, being capable of solving more instances than state-of-theart MaxSAT solvers. © 2014 Springer International Publishing Switzerland.
978-3-319-10427-0
978-3-319-10428-7
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11770/295577
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 69
  • ???jsp.display-item.citation.isi??? 56
social impact