On CDCL-Based Proof Systems with the Ordered Decision Strategy
| Autor: | Alexander A. Razborov, Shuo Pang, Nathan Mull |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Scheme (programming language)
050101 languages & linguistics Unit propagation Computer science media_common.quotation_subject 05 social sciences 02 engineering and technology Solver Resolution (logic) Conflict analysis Presentation TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Decision strategy 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Algorithm computer computer.programming_language media_common |
| Zdroj: | Theory and Applications of Satisfiability Testing – SAT 2020 ISBN: 9783030518240 SAT |
| Popis: | We prove that CDCL SAT-solvers with the ordered decision strategy and the DECISION learning scheme are equivalent to ordered resolution. We also prove that, by replacing this learning scheme with its opposite, which learns the first possible non-conflict clause, they become equivalent to general resolution. In both results, we allow nondeterminism in the solver’s ability to perform unit propagation, conflict analysis, and restarts in a way that is similar to previous works in the literature. To aid the presentation of our results, and possibly future research, we define a model and language for CDCL-based proof systems – particularly those with nonstandard features – that allow for succinct and precise theorem statements. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|