- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- BIRS Workshop Lecture Videos /
- The Proof Complexity of SMT Solvers
Open Collections
BIRS Workshop Lecture Videos
BIRS Workshop Lecture Videos
The Proof Complexity of SMT Solvers Kolokolova, Antonina
Description
The resolution proof system has been enormously helpful in deepening our
understanding of conflict-driven clause-learning (CDCL) SAT solvers. In the
interest of providing a similar proof complexity-theoretic analysis of
satisfiability modulo theories (SMT) solvers, we introduce a generalization
of resolution called Res(T). We show that many of the known results
comparing resolution and CDCL solvers lift to the SMT setting, such as the
result of Pipatsrisawat and Darwiche showing that CDCL solvers with
``perfect'' non-deterministic branching and an asserting clause-learning
scheme can polynomially simulate general resolution. We also describe a
stronger version of Res(T), Res*(T), capturing SMT solvers allowing
introduction of new literals.
We analyze the theory EUF of equality with uninterpreted functions, and
show that the Res*(EUF) system is able to simulate an earlier calculus
introduced by Bjorner and De Moura for the purpose of analyzing DPLL(EUF).
Further, we show that Res*(EUF) (and thus SMT algorithms with clause
learning over EUF, new literal introduction rules and perfect branching)
can simulate the Frege proof system, which is well-known to be far more
powerful than resolution. Finally, we prove under the Exponential Time
Hypothesis (ETH) that any reduction from EUF to SAT (such as the Ackermann
reduction) must, in the worst case, produce an instance of size at least n
log n from an instance of size n.
Item Metadata
| Title |
The Proof Complexity of SMT Solvers
|
| Creator | |
| Publisher |
Banff International Research Station for Mathematical Innovation and Discovery
|
| Date Issued |
2018-08-30T17:04
|
| Description |
The resolution proof system has been enormously helpful in deepening our
understanding of conflict-driven clause-learning (CDCL) SAT solvers. In the
interest of providing a similar proof complexity-theoretic analysis of
satisfiability modulo theories (SMT) solvers, we introduce a generalization
of resolution called Res(T). We show that many of the known results
comparing resolution and CDCL solvers lift to the SMT setting, such as the
result of Pipatsrisawat and Darwiche showing that CDCL solvers with
``perfect'' non-deterministic branching and an asserting clause-learning
scheme can polynomially simulate general resolution. We also describe a
stronger version of Res(T), Res*(T), capturing SMT solvers allowing
introduction of new literals.
We analyze the theory EUF of equality with uninterpreted functions, and show that the Res*(EUF) system is able to simulate an earlier calculus introduced by Bjorner and De Moura for the purpose of analyzing DPLL(EUF). Further, we show that Res*(EUF) (and thus SMT algorithms with clause learning over EUF, new literal introduction rules and perfect branching) can simulate the Frege proof system, which is well-known to be far more powerful than resolution. Finally, we prove under the Exponential Time Hypothesis (ETH) that any reduction from EUF to SAT (such as the Ackermann reduction) must, in the worst case, produce an instance of size at least n log n from an instance of size n. |
| Extent |
32.0
|
| Subject | |
| Type | |
| File Format |
video/mp4
|
| Language |
eng
|
| Notes |
Author affiliation: Memorial University of Newfoundland
|
| Series | |
| Date Available |
2019-04-05
|
| Provider |
Vancouver : University of British Columbia Library
|
| Rights |
Attribution-NonCommercial-NoDerivatives 4.0 International
|
| DOI |
10.14288/1.0377824
|
| URI | |
| Affiliation | |
| Peer Review Status |
Unreviewed
|
| Scholarly Level |
Faculty
|
| Rights URI | |
| Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International