Improving IntSat by expressing disjunctions of bounds as linear constraints
Visualitza/Obre
p.pdf (234,9Kb) (Accés restringit)
Sol·licita una còpia a l'autor
Què és aquest botó?
Aquest botó permet demanar una còpia d'un document restringit a l'autor. Es mostra quan:
- Disposem del correu electrònic de l'autor
- El document té una mida inferior a 20 Mb
- Es tracta d'un document d'accés restringit per decisió de l'autor o d'un document d'accés restringit per política de l'editorial
Cita com:
hdl:2117/103144
Tipus de documentArticle
Data publicació2016
Condicions d'accésAccés restringit per política de l'editorial
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
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. This obviously strengthens learning and significantly improves the performance of IntSat (as confirmed by our experiments). We also briefly discuss extensions and other applications.
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.
ISSN0921-7126
Versió de l'editorhttp://content.iospress.com/articles/ai-communications/aic684
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
p.pdf | 234,9Kb | Accés restringit |