Universitat de Lleida
    • English
    • català
    • español
  • català 
    • English
    • català
    • español
  • Inicia la sessió
Repositori Obert UdL
Visualitza l'element 
  •   Inici
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • Visualitza l'element
  •   Inici
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • Visualitza l'element
JavaScript is disabled for your browser. Some features of this site may not work without it.

New Inference Rules for Max-SAT

Thumbnail
Visualitza/Obre
012470.pdf (391.0Kb)
Sol·licita una còpia
Data de publicació
2007
Autor/a
Li, Chu-Min
Manyà Serres, Felip
Planes Cid, Jordi
Citació recomanada
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.
Impacte


Logo de Web of Science    citacions a Web of Science

Logo d'Scopus    citacions a Scopus

Logo de Google Acadèmic  Google Acadèmic
Compartir
Exportar a Mendeley
Metadades
Mostra el registre d'unitat complet
Resum
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
És part de
Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359
Projectes de recerca europeus
Col·leccions
  • Grup de Recerca en Energia i Intel·ligència Artificial (GREiA) (INSPIRES) [382]
  • Articles publicats (Informàtica i Enginyeria Industrial) [769]
  • Publicacions de projectes de recerca del Plan Nacional [2215]

Publicacions relacionades

Mostrant elements relacionats per títol, autor i matèria.

  • The first and second Max-SAT evaluations 

    Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (IOS Press, 2008)
    We describe the organization and report on the results of the First and Second Max-SAT Evaluations, which were organized as affiliated events of the 2006 and 2007 editions of the International Conference on Theory and ...
  • Analyzing the instances of the MaxSAT evaluation 

    Argelich Romà, Josep; Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2011)
    The MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: MaxSAT, ...
  • Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers 

    Li, Chu-Min; Manyà Serres, Felip; Planes Cid, Jordi (Springer Verlag, 2005)
    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, ...

Contacteu amb nosaltres | Envia comentaris | Avís legal
© 2021 BiD. Universitat de Lleida
Metadades subjectes a 
 

 

Explora

Tot el repositoriComunitats i col·leccionsPer data d'edicióAutorsTítolsMatèriesAquesta col·leccióPer data d'edicióAutorsTítolsMatèries

Estadístiques

Veure estadístiques d'ús

D'interès

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

Contacteu amb nosaltres | Envia comentaris | Avís legal
© 2021 BiD. Universitat de Lleida
Metadades subjectes a