Assessing progress in SAT solvers through the lens of incremental SAT

Stepan Kochemazov, Alexey Ignatiev, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)


There is a wide consensus, which is supported by the hard experimental evidence of the SAT competitions, that clear progress in SAT solver performance has been observed in recent years. However, in the vast majority of practical applications of SAT, one is expected to use SAT solvers as oracles deciding a possibly large number of propositional formulas. In practice, this is often achieved through the use of incremental SAT. Given this fundamental use of SAT solvers, this paper investigates whether recent improvements in solver performance have an observable positive impact on the overall problem-solving efficiency in settings where incremental SAT is mandatory or at least expected. Our results, obtained on a number of well-known practically significant applications, suggest that most improvements made to SAT solvers in recent years have no positive impact on the overall performance when solvers are used incrementally.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2021
Subtitle of host publication24th International Conference Barcelona, Spain, July 5–9, 2021 Proceedings
EditorsChu-Min Li, Felip Manyà
Place of PublicationCham Switzerland
Number of pages19
ISBN (Electronic)9783030802233
ISBN (Print)9783030802226
Publication statusPublished - 2021
EventInternational Conference on Theory and Applications of Satisfiability Testing 2021 - Barcelona, Spain
Duration: 5 Jul 20219 Jul 2021
Conference number: 24th (Proceedings)

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2021
Abbreviated titleSAT 2021
Internet address

Cite this