Cargando…
On CDCL-Based Proof Systems with the Ordered Decision Strategy
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 res...
| Autores principales: | , , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
2020
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326566/ http://dx.doi.org/10.1007/978-3-030-51825-7_12 |