Universitat de Lleida
    • English
    • català
    • español
  • English 
    • English
    • català
    • español
  • Login
Repositori Obert UdL
View Item 
  •   Home
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • View Item
  •   Home
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers

Thumbnail
View/Open
007814.pdf (219.8Kb)
Sol·licita una còpia
Issue date
2005
Author
Li, Chu-Min
Manyà Serres, Felip
Planes Cid, Jordi
Suggested citation
Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi; . (2005) . Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers. Lecture Notes in Computer Science, 2005, vol. 3709, p. 403-414. https://doi.org/10.1007/11564751_31.
Impact


Web of Science logo    citations in Web of Science

Scopus logo    citations in Scopus

Google Scholar logo  Google Scholar
Share
Export to Mendeley
Metadata
Show full item record
Abstract
One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensure optimality, can only apply unit propagation to a restricted number of nodes. In this paper, we describe a branch and bound MaxSAT solver that applies unit propagation at each node of the proof tree to compute the lower bound instead of applying unit propagation to simplify the formula. The new lower bound captures the lower bound based on inconsistency counts that apply most of the state-of-the-art Max-SAT solvers as well as other improvements, like the start rule, that have been defined to get a lower bound of better quality. Moreover, our solver incorporates the Jeroslow-Wang variable selection heuristic, the pure literal and dominating unit clause rules, and novel preprocessing techniques. The experimental investigation we conducted to compare our solver with the most modern Max-SAT solvers provides experimental evidence that our solver is very competitive.
URI
http://hdl.handle.net/10459.1/57574
DOI
https://doi.org/10.1007/11564751_31
Is part of
Lecture Notes in Computer Science, 2005, vol. 3709, p. 403-414
European research projects
Collections
  • Articles publicats (Informàtica i Enginyeria Industrial) [933]
  • Publicacions de projectes de recerca del Plan Nacional [2653]
  • Grup de Recerca en Energia i Intel·ligència Artificial (GREiA) (INSPIRES) [444]

Contact Us | Send Feedback | Legal Notice
© 2022 BiD. Universitat de Lleida
Metadata subjected to 
 

 

Browse

All of the repositoryCommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

Statistics

View Usage Statistics

D'interès

Política institucional d'accés obertDiposita les teves publicacionsDiposita dades de recercaSuport a la recerca

Contact Us | Send Feedback | Legal Notice
© 2022 BiD. Universitat de Lleida
Metadata subjected to