Carregant...
Carregant...

Vés al contingut (premeu Retorn)

Trade-offs between time and memory in a tighter model of CDCL SAT solvers

Autor
Elffers, J.; Johannsen, J.; Lauria, M.; Magnard, T.; Nordström, J.; Vinyals, M.
Tipus d'activitat
Presentació treball a congrés
Nom de l'edició
19th International Conference on Theory and Applications of Satisfiability Testing
Any de l'edició
2016
Data de presentació
2016-07
Llibre d'actes
Theory and Applications of Satisfiability Testing – SAT 2016, 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
Pàgina inicial
160
Pàgina final
176
DOI
https://doi.org/10.1007/978-3-319-40970-2_11 Obrir en finestra nova
Repositori
http://hdl.handle.net/2117/103872 Obrir en finestra nova
URL
http://link.springer.com/chapter/10.1007%2F978-3-319-40970-2_11 Obrir en finestra nova
Resum
"The final publication is available at http://link.springer.com/chapter/10.1007/978-3-319-40970-2_11 A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are...
Citació
Elffers, J., Johannsen, J., Lauria, M., Magnard, T., Nordström, J., Vinyals, M. Trade-offs between time and memory in a tighter model of CDCL SAT solvers. A: International Conference on Theory and Applications of Satisfiability Testing. "Theory and Applications of Satisfiability Testing – SAT 2016, 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings". Bordeaux: 2016, p. 160-176.
Paraules clau
Commerce, Formal Logic, Clause Learning, Fine Grained, Learning Schemes, Lower Bounds, Memory Usage, Resolution Proofs, Sat Solvers, Upper Bound, Economic And Social Effects
Grup de recerca
ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals

Participants

  • Elffers, J.  (autor ponent)
  • Johannsen, Jan  (autor ponent)
  • Lauria, Massimo  (autor ponent)
  • Magnard, Thomas  (autor ponent)
  • Nordström, Jakob  (autor ponent)
  • Vinyals, Marc  (autor ponent)

Arxius