In this preliminary paper we describe a general approach for multiple learning in conflict-driven SAT solvers. The proposed formulation of the conflict analysis task turns out to be expressive enough to reckon with different orthogonal generalizations of the standard learning schemata, such as the conjunct analysis of multiple conflicts, the generation of possibly interdependent learned clauses, the imposition of global optimality criteria. We formalize the general learning problem as a search for a collection of vertex cuts in a directed acyclic graph. Optimality of the solution may be evaluated with respect to a given global objective function intended to encode search strategies and heuristics affecting the behavior of the solver. We also outline some algo-rithmical solutions by exploiting standard algorithms proposed to solve cut and multicut problems on DAGs.

On multiple learning schemata in conflict driven solvers / Formisano, A.; Vella, F.. - 1231:(2014), pp. 133-146. (Intervento presentato al convegno 15th Italian Conference on Theoretical Computer Science, ICTCS 2014 tenutosi a Perugia, Italy nel 17–19 September 2014).

On multiple learning schemata in conflict driven solvers

Vella F.
2014-01-01

Abstract

In this preliminary paper we describe a general approach for multiple learning in conflict-driven SAT solvers. The proposed formulation of the conflict analysis task turns out to be expressive enough to reckon with different orthogonal generalizations of the standard learning schemata, such as the conjunct analysis of multiple conflicts, the generation of possibly interdependent learned clauses, the imposition of global optimality criteria. We formalize the general learning problem as a search for a collection of vertex cuts in a directed acyclic graph. Optimality of the solution may be evaluated with respect to a given global objective function intended to encode search strategies and heuristics affecting the behavior of the solver. We also outline some algo-rithmical solutions by exploiting standard algorithms proposed to solve cut and multicut problems on DAGs.
2014
CEUR Workshop Proceedings
Aachen, Germany
CEUR-WS
Formisano, A.; Vella, F.
On multiple learning schemata in conflict driven solvers / Formisano, A.; Vella, F.. - 1231:(2014), pp. 133-146. (Intervento presentato al convegno 15th Italian Conference on Theoretical Computer Science, ICTCS 2014 tenutosi a Perugia, Italy nel 17–19 September 2014).
File in 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/11572/332828
 Attenzione

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

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