@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@inproceedings{YSBSM23,
  author={Yang, Jiong and Shaw, Arijit and Baluta, Teodora and Soos, Mate and Meel, Kuldeep S.},
  title={Explaining SAT Solving Using Causal Reasoning},
  abstract={The past three decades have witnessed notable success in designing efficient SAT solvers, 
    with modern solvers capable of solving industrial benchmarks containing millions of variables in 
  just a few seconds. The success of modern SAT solvers owes to the widely-used CDCL algorithm, which 
 lacks comprehensive theoretical investigation. Furthermore, it has been observed that CDCL solvers still 
struggle to deal with specific classes of benchmarks comprising only hundreds of variables, which contrasts
with their widespread use in real-world applications. Consequently, there is an urgent need to uncover the 
inner workings of these seemingly weak yet powerful black boxes.
In this paper, we present a first step towards this goal by introducing an approach called 
CausalSAT, which employs causal reasoning to gain insights into the functioning of modern 
SAT solvers. CausalSAT initially generates observational data from the execution of SAT solvers 
and learns a structured graph representing the causal relationships between the components of an 
SAT solver. Subsequently, given a query such as whether a clause with low literals blocks distance 
(LBD) has a higher clause utility, CausalSAT calculates the causal effect of LBD on clause utility 
and provides an answer to the question. We utilize CausalSAT to quantitatively verify hypotheses 
previously regarded as “rules of thumb” or empirical findings, such as the query above or the notion 
that clauses with high LBD experience a rapid drop in utility over time. Moreover, CausalSAT can 
address previously unexplored questions, like which branching heuristic results in greater clause 
utility in order to study the relationship between branching and clause management. Experimental 
evaluations using practical benchmarks demonstrate that CausalSAT effectively fits the data, 
verifies four “rules of thumb”, and provides answers to three questions closely related to implementing modern solvers.},
year={2023},
month=jul,
booktitle=SAT,
bib2html_pubtype={Refereed Conference},
bib2html_rescat={Solver Engineering},
bib2html_dl_pdf={https://arxiv.org/pdf/2306.06294.pdf},
}