Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Limits of CDCL learning via merge resolution

Vinyals, Marc ; Li, Chunxiao ; Fleming, Noah LU orcid ; Kolokolova, Antonina and Ganesh, Vijay (2023) In LIPIcs 271. p.1-27
Abstract
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such... (More)
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs. (Less)
Please use this url to cite or link to this publication:
author
; ; ; and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
host publication
The International Conferences on Theory and Applications of Satisfiability Testing
series title
LIPIcs
volume
271
pages
19 pages
publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
external identifiers
  • scopus:85170570603
DOI
10.4230/LIPICS.SAT.2023.27
language
English
LU publication?
no
id
95f4df80-baa5-4e78-a91a-e9d3cdc8ee6d
date added to LUP
2025-11-05 15:49:39
date last changed
2026-08-15 04:01:26
@inproceedings{95f4df80-baa5-4e78-a91a-e9d3cdc8ee6d,
  abstract     = {{In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.}},
  author       = {{Vinyals, Marc and Li, Chunxiao and Fleming, Noah and Kolokolova, Antonina and Ganesh, Vijay}},
  booktitle    = {{The International Conferences on Theory and Applications of Satisfiability Testing}},
  language     = {{eng}},
  pages        = {{1--27}},
  publisher    = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
  series       = {{LIPIcs}},
  title        = {{Limits of CDCL learning via merge resolution}},
  url          = {{http://dx.doi.org/10.4230/LIPICS.SAT.2023.27}},
  doi          = {{10.4230/LIPICS.SAT.2023.27}},
  volume       = {{271}},
  year         = {{2023}},
}