SwePub
Sök i LIBRIS databas

  Utökad sökning

onr:"swepub:oai:DiVA.org:kth-195488"
 

Sökning: onr:"swepub:oai:DiVA.org:kth-195488" > Trade-offs between ...

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

Elffers, Jan (författare)
KTH,Teoretisk datalogi, TCS
Johannsen, J. (författare)
Lauria, M. (författare)
visa fler...
Magnard, T. (författare)
Nordström, Jakob (författare)
KTH,Teoretisk datalogi, TCS
Vinyals, Marc (författare)
KTH,Teoretisk datalogi, TCS
visa färre...
 (creator_code:org_t)
2016-06-11
2016
Engelska.
Ingår i: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016. - Cham : Springer. - 9783319409696 ; , s. 160-176
  • Konferensbidrag (refereegranskat)
Abstract Ämnesord
Stäng  
  • 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 frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that cap- tures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL with- out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Nyckelord

Commerce
Formal logic
Clause learning
Fine grained
Learning schemes
Lower bounds
Memory usage
Resolution proofs
SAT solvers
Upper Bound
Economic and social effects

Publikations- och innehållstyp

ref (ämneskategori)
kon (ämneskategori)

Hitta via bibliotek

Till lärosätets databas

Sök utanför SwePub

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Stäng

Kopiera och spara länken för att återkomma till aktuell vy