- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- BIRS Workshop Lecture Videos /
- On CDCL-based Proof Systems with the Ordered Decision...
Open Collections
BIRS Workshop Lecture Videos
BIRS Workshop Lecture Videos
On CDCL-based Proof Systems with the Ordered Decision Strategy Mull, Nathan
Description
It has been well-established that CDCL SAT solvers with restarts can simulate general resolution.
However, these results require that the solver use a highly nondeterministic or sufficiently random decision strategy.
Our goal is to understand the impact of more explicit decision strategies on the theoretical strength of CDCL.
Since decisions strategies used in practice are somewhat complicated, we instead focus on the simpler ordered decision strategy: when the solver has to choose a variable to assign, it must choose the smallest unassigned variable according to some underlying order.
This strategy was studied by Beame et. al. (2002) in the context of DLL without clause learning.
It is still possible for unit propagation to assign variables out of order, which is what makes this situation more subtle and non-trivial.
Our motivating question is the following: is there a family of unsatisfiable formulas that possess polynomial size resolution refutations but require super-polynomial time for CDCL using the ordered decision strategy
We present preliminary results towards this end.
First, we show that CDCL with the ordered decision strategy and the so-called DECISION learning scheme is no more powerful than ordered resolution.
Second, we show that CDCL with the ordered decision strategy and a somewhat powerful learning scheme we call FIRST-L (similar to FirstNewCut introduced by Beame et. al. (2004)) is equivalent to general resolution, given it can ignore unit clauses and conflicts.
This result may be interpreted as demonstrating that mandatory unit propagation or conflict analysis is, in some sense, necessary to positively answer our the question above.
To aid this work, we also present a model and language for discussing CDCL-based proof systems. This is not meant to be novel and is heavily influenced by previous works. But rather than being faithful to practical SAT-solver implementations, the goal of our model is highlighting possible non-standard sources of nondeterminism. It allows for clear and concise mathematical statements about CDCL-based proof systems and better represents the landscape of potential CDCL variants.
Item Metadata
| Title |
On CDCL-based Proof Systems with the Ordered Decision Strategy
|
| Creator | |
| Publisher |
Banff International Research Station for Mathematical Innovation and Discovery
|
| Date Issued |
2018-08-30T17:40
|
| Description |
It has been well-established that CDCL SAT solvers with restarts can simulate general resolution.
However, these results require that the solver use a highly nondeterministic or sufficiently random decision strategy.
Our goal is to understand the impact of more explicit decision strategies on the theoretical strength of CDCL.
Since decisions strategies used in practice are somewhat complicated, we instead focus on the simpler ordered decision strategy: when the solver has to choose a variable to assign, it must choose the smallest unassigned variable according to some underlying order.
This strategy was studied by Beame et. al. (2002) in the context of DLL without clause learning.
It is still possible for unit propagation to assign variables out of order, which is what makes this situation more subtle and non-trivial.
Our motivating question is the following: is there a family of unsatisfiable formulas that possess polynomial size resolution refutations but require super-polynomial time for CDCL using the ordered decision strategy We present preliminary results towards this end. First, we show that CDCL with the ordered decision strategy and the so-called DECISION learning scheme is no more powerful than ordered resolution. Second, we show that CDCL with the ordered decision strategy and a somewhat powerful learning scheme we call FIRST-L (similar to FirstNewCut introduced by Beame et. al. (2004)) is equivalent to general resolution, given it can ignore unit clauses and conflicts. This result may be interpreted as demonstrating that mandatory unit propagation or conflict analysis is, in some sense, necessary to positively answer our the question above. To aid this work, we also present a model and language for discussing CDCL-based proof systems. This is not meant to be novel and is heavily influenced by previous works. But rather than being faithful to practical SAT-solver implementations, the goal of our model is highlighting possible non-standard sources of nondeterminism. It allows for clear and concise mathematical statements about CDCL-based proof systems and better represents the landscape of potential CDCL variants. |
| Extent |
29.0
|
| Subject | |
| Type | |
| File Format |
video/mp4
|
| Language |
eng
|
| Notes |
Author affiliation: University of Chicago
|
| Series | |
| Date Available |
2019-04-05
|
| Provider |
Vancouver : University of British Columbia Library
|
| Rights |
Attribution-NonCommercial-NoDerivatives 4.0 International
|
| DOI |
10.14288/1.0377825
|
| URI | |
| Affiliation | |
| Peer Review Status |
Unreviewed
|
| Scholarly Level |
Graduate
|
| Rights URI | |
| Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International