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.

New Inference Rules for Max-SAT

Thumbnail
View/Open
012470.pdf (391.0Kb)
Sol·licita una còpia
Issue date
2007
Author
Li, Chu-Min
Manyà Serres, Felip
Planes Cid, Jordi
Suggested citation
Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi; . (2007) . New Inference Rules for Max-SAT. Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359. https://doi.org/10.1613/jair.2215.
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
Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, MaxCut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.
URI
http://hdl.handle.net/10459.1/57413
DOI
https://doi.org/10.1613/jair.2215
Is part of
Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359
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