Vés al contingut (premeu Retorn)

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

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ó
Data de presentació
Llibre d'actes
Theory and Applications of Satisfiability Testing – SAT 2016, 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings
Pàgina inicial
Pàgina final
DOI Obrir en finestra nova
Repositori Obrir en finestra nova
URL Obrir en finestra nova
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 ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very ...
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


  • 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)