|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'504'585
Articles rated: 2609
25 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
A Concurrency Problem with Exponential DPLL(T) Proofs | | Liana Hadarean
; Alex Horn
; Tim King
; | | Date: |
4 Jun 2015 | | Abstract: | Many satisfiability modulo theories solvers implement a variant of the DPLL(T
) framework which separates theory-specific reasoning from reasoning on the
propositional abstraction of the formula. Such solvers conclude that a formula
is unsatisfiable once they have learned enough theory conflicts to derive a
propositional contradiction. However some problems, such as the diamonds
problem, require learning exponentially many conflicts. We give a general
criterion for establishing lower bounds on the number of theory conflicts in
any DPLL(T ) proof for a given problem. We apply our criterion to two different
state-of-the-art symbolic partial-order encodings of a simple, yet
representative concurrency problem. Even though one of the encodings is
asymptotically smaller than the other, we establish the same exponential lower
bound proof complexity for both. Our experiments confirm this theoretical lower
bound across multiple solvers and theory combinations. | | Source: | arXiv, 1506.1602 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER