Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Improving IntSat by expressing disjunctions of bounds as linear constraints

Autor
Asín, R.J.; Aloysius, M.; Nieuwenhuis, R.
Tipus d'activitat
Article en revista
Revista
AI communications: the european journal of artificial intelligence
Data de publicació
2016
Volum
29
Número
1
Pàgina inicial
205
Pàgina final
209
DOI
https://doi.org/10.3233/AIC-150684 Obrir en finestra nova
Repositori
http://hdl.handle.net/2117/103144 Obrir en finestra nova
URL
http://content.iospress.com/articles/ai-communications/aic684 Obrir en finestra nova
Resum
Conflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates no strong enough ILP constraint, and the backjump has to be done based on the conflicting set of bounds. The techniques given in this article precisely analyze how and when that set can be translated into the required new ILP constraint. Moreover, this can be done efficiently. ...
Citació
Asín, R.J., Aloysius, M., Nieuwenhuis, R. Improving IntSat by expressing disjunctions of bounds as linear constraints. "AI communications: the european journal of artificial intelligence", 2016, vol. 29, núm. 1, p. 205-209.
Paraules clau
SAT, conflict-driven clause learning, constraint programming, integer linear programming
Grup de recerca
LOGPROG - Lògica i Programació