Universitat de Lleida
    • English
    • català
    • español
  • español 
    • English
    • català
    • español
  • Iniciar sesión
Repositori Obert UdL
Ver ítem 
  •   Inicio
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • Ver ítem
  •   Inicio
  • Recerca
  • Informàtica i Enginyeria Industrial
  • Articles publicats (Informàtica i Enginyeria Industrial)
  • Ver ítem
JavaScript is disabled for your browser. Some features of this site may not work without it.

New Inference Rules for Max-SAT

Thumbnail
Ver/Abrir
012470.pdf (391.0Kb)
Sol·licita una còpia
Fecha de publicación
2007
Autor/a
Li, Chu-Min
Manyà Serres, Felip
Planes Cid, Jordi
Cita recomendada
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.
Impacto


Logo de Web of Science    citaciones en Web of Science

Logo de Scopus    citaciones en Scopus

Logo de Google Académico  Google Académico
Compartir
Exportar a Mendeley
Metadatos
Mostrar el registro completo del ítem
Resumen
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
Es parte de
Journal of Artificial Intelligence Research, 2007, vol. 30, p. 321-359
Proyectos de investigación europeos
Colecciones
  • 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]

Publicaciones relacionadas

Showing items related by title, author, creator and subject.

  • 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, ...

Contacto | Sugerencias | Aviso legal
© 2021 BiD. Universitat de Lleida
Metadatos sujetos a 
 

 

Explorar

Todo el repositorioComunidades y coleccionesPor fecha de publicaciónAutoresTítulosMateriasEsta colecciónPor fecha de publicaciónAutoresTítulosMaterias

Estadísticas

Ver Estadísticas de uso

De interés

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

Contacto | Sugerencias | Aviso legal
© 2021 BiD. Universitat de Lleida
Metadatos sujetos a