An approach to propositional satisfiability using an adaptive procedure is described. Its main feature is a new branching rule, which is able to identify, at an early stage, hard sub-formulae. Such branching rule is based on a simple and easy computable criterion, whose merit function is updated by a learning mechanism, and guides the exploration of a clause-based branching tree. Completeness is guaranteed. Moreover, a new search technique named core search is used to speed-up the above procedure while preserving completeness. This is inspired by the well-known approaches of row and column generation used in mathematical programming. Encouraging computational results and comparisons are presented.

A Complete Adaptive Algorithm for Propositional Satisfiability / Bruni, Renato; Sassano, Antonio. - In: DISCRETE APPLIED MATHEMATICS. - ISSN 0166-218X. - STAMPA. - 127:(2003), pp. 523-534. [10.1016/S0166-218X(02)00385-2]

A Complete Adaptive Algorithm for Propositional Satisfiability

BRUNI, Renato
;
SASSANO, Antonio
2003

Abstract

An approach to propositional satisfiability using an adaptive procedure is described. Its main feature is a new branching rule, which is able to identify, at an early stage, hard sub-formulae. Such branching rule is based on a simple and easy computable criterion, whose merit function is updated by a learning mechanism, and guides the exploration of a clause-based branching tree. Completeness is guaranteed. Moreover, a new search technique named core search is used to speed-up the above procedure while preserving completeness. This is inspired by the well-known approaches of row and column generation used in mathematical programming. Encouraging computational results and comparisons are presented.
2003
Backtracking; Search frameworks; Satisfiability
01 Pubblicazione su rivista::01a Articolo in rivista
A Complete Adaptive Algorithm for Propositional Satisfiability / Bruni, Renato; Sassano, Antonio. - In: DISCRETE APPLIED MATHEMATICS. - ISSN 0166-218X. - STAMPA. - 127:(2003), pp. 523-534. [10.1016/S0166-218X(02)00385-2]
File allegati a 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/11573/427909
 Attenzione

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

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