Date & Time:
November 26, 2019 10:30 am – 11:30 am
Crerar 298, 5730 S. Ellis Ave., Chicago, IL,
11/26/2019 10:30 AM 11/26/2019 11:30 AM America/Chicago MS Presentation: Nathan Mull Crerar 298, 5730 S. Ellis Ave., Chicago, IL,

CDCL SAT Solvers, Subsystem of Resolution, and the
Ordered Decision Strategy

Despite the NP-hardness of SAT, algorithms for SAT (SAT solvers) have
become standard tools in industrial settings and are even sometimes
used as NP oracles. Due to their success, there is increased interest
in understanding why they work so well and, moreover, if there is any
theoretical justification for the performance seen in practice. We
consider an approach which relates variants of a particular
algorithmic framework for SAT solving to subsystems of the resolution
proof system. In particular, so-called CDCL solvers, when run on
unsatisfiable formulas, may be thought of as generating proofs of
unsatisfiability, so their refutational strength can be studied using
tools from propositional proof complexity.

We focus on CDCL solvers using a heuristic called the ordered decision
strategy. We prove that such solvers, when also using a heuristic
called the DECISION learning strategy, are not as refutationally
powerful as resolution. We also prove that they become as powerful as
resolution when granted a different learning strategy and
nondeterminism in certain parts of the algorithm. This second results
may be viewed as showing that a natural target for proving separations
between resolution and CDCL solvers with the ordered decision strategy
ultimately fails. To aid the presentation of these results as well as
future work, we present a flexible model and associated notation for
CDCL solvers that allows for succinct and precise theorem statements.

All results are based on joint work with Professor Alexander Razborov
and Shuo Pang.

Nathan Mull

M.S. Candidate, University of Chicago

Nathan's advisor is Prof. Stuart Kurtz

Related News & Events

UChicago CS News

Five UChicago CS students named to Siebel Scholars Class of 2024

Oct 02, 2023
UChicago CS News

UChicago Computer Scientists Bring in Generative Neural Networks to Stop Real-Time Video From Lagging

Jun 29, 2023
UChicago CS News

UChicago Team Wins The NIH Long COVID Computational Challenge

Jun 28, 2023
UChicago CS News

UChicago Assistant Professor Raul Castro Fernandez Receives 2023 ACM SIGMOD Test-of-Time Award

Jun 27, 2023
UChicago CS News

Computer Science Displays Catch Attention at MSI’s Annual Robot Block Party

Apr 07, 2023
Students posing at competition
UChicago CS News

UChicago Undergrad Team Places Second Overall In Regionals For World’s Largest Programming Competition

Mar 17, 2023
UChicago CS News

Professor Heather Zheng Named ACM Fellow

Jan 18, 2023

Ian Foster – Better Information Faster: Programming the Continuum

Jan 06, 2023
UChicago CS News

Q&A: Ian Foster on Receiving the 2023 IEEE Internet Award

Jan 06, 2023
UChicago CS News

Professor Fred Chong Named IEEE Fellow

Dec 09, 2022
UChicago CS News

Associate Professor Diana Franklin Named ACM Distinguished Member

Dec 07, 2022
Haifeng Xu
UChicago CS News

New CS and DSI Faculty Haifeng Xu Brings Strategic Intelligence to NeurIPS 2022

Nov 28, 2022
arrow-down-largearrow-left-largearrow-right-large-greyarrow-right-large-yellowarrow-right-largearrow-right-smallbutton-arrowclosedocumentfacebookfacet-arrow-down-whitefacet-arrow-downPage 1CheckedCheckedicon-apple-t5backgroundLayer 1icon-google-t5icon-office365-t5icon-outlook-t5backgroundLayer 1icon-outlookcom-t5backgroundLayer 1icon-yahoo-t5backgroundLayer 1internal-yellowinternalintranetlinkedinlinkoutpauseplaypresentationsearch-bluesearchshareslider-arrow-nextslider-arrow-prevtwittervideoyoutube