Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Automated benchmarking of incremental SAT and QBF solvers
Institute of Information Systems 184/3, Vienna University of Technology, Vienna, Austria.
Institute of Information Systems 184/3, Vienna University of Technology, Vienna, Austria.
Institute of Information Systems 184/3, Vienna University of Technology, Vienna, Austria.ORCID-id: 0000-0002-9902-7662
2015 (engelsk)Inngår i: Logic for Programming, Artificial Intelligence, and Reasoning: 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings / [ed] M. Davis, A. Fehnker, A. McIver & A. Voronkov, Springer, 2015, s. 178-186Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

Incremental SATandQBF solving potentially yields improvements when sequences of related formulas are solved. An incremental application is usually tailored towards some specific solver and decomposes a problem into incremental solver calls. This hinders the independent comparison of different solvers, particularly when the application program is not available. As a remedy, we present an approach to automated benchmarking of incremental SAT and QBF solvers.Given a collection of formulas in (Q)DIMACS format generated incrementally by an application program, our approach automatically translates the formulas into instructions to import and solve a formula by an incremental SAT/QBF solver. The result of the translation is a program which replays the incremental solver calls and thus allows to evaluate incremental solvers independently from the application program.We illustrate our approach by different hardware verification problems for SAT and QBF solvers.

sted, utgiver, år, opplag, sider
Springer, 2015. s. 178-186
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 9450
Emneord [en]
Application programs, Artificial intelligence, Boolean functions, Computer circuits, Program translators, Reconfigurable hardware, Hardware verification, QBF solvers, Benchmarking
HSV kategori
Identifikatorer
URN: urn:nbn:se:hj:diva-63565DOI: 10.1007/978-3-662-48899-7_13Scopus ID: 2-s2.0-84952673899ISBN: 9783662488980 (tryckt)OAI: oai:DiVA.org:hj-63565DiVA, id: diva2:1838441
Konferanse
20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015
Tilgjengelig fra: 2024-02-16 Laget: 2024-02-16 Sist oppdatert: 2024-02-16bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Person

Oetsch, Johannes

Søk i DiVA

Av forfatter/redaktør
Oetsch, Johannes

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 7 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf