Incremental Inprocessing SAT Solving

Katalin Fazekas; Armin Biere; Christoph Scholl

Incremental Inprocessing SAT Solving

Katalin Fazekas
, Armin Biere
, Christoph Scholl

Institute of Formal Models and Verification

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

Incremental SAT is about solving a sequence of related SAT problems eﬃciently. It makes use of already learned information to avoid repeating redundant work. Also preprocessing and inprocessing are considered to be crucial. Our calculus uses the most general redundancy property and extends existing inprocessing rules to incremental SAT solving. It allows to automatically reverse earlier simpliﬁcation steps, which are inconsistent with literals in new incrementally added clauses. Our approach to incremental SAT solving not only simpliﬁes the use of inprocessing but also substantially improves solving time.

Original language	English
Title of host publication	Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19)
Editors	Mikoláš Janota, Inês Lynce
Publisher	Springer
Pages	136-154
Number of pages	19
Volume	11628
ISBN (Print)	978-3-030-24257-2
Publication status	Published - Jul 2019

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102031 Theoretical computer science
603109 Logic
202006 Computer hardware

Cite this

@inproceedings{9da5e20be55342bd8b0bb015a3f1095c,

title = "Incremental Inprocessing SAT Solving",

abstract = "Incremental SAT is about solving a sequence of related SAT problems eﬃciently. It makes use of already learned information to avoid repeating redundant work. Also preprocessing and inprocessing are considered to be crucial. Our calculus uses the most general redundancy property and extends existing inprocessing rules to incremental SAT solving. It allows to automatically reverse earlier simpliﬁcation steps, which are inconsistent with literals in new incrementally added clauses. Our approach to incremental SAT solving not only simpliﬁes the use of inprocessing but also substantially improves solving time.",

author = "Katalin Fazekas and Armin Biere and Christoph Scholl",

year = "2019",

month = jul,

language = "English",

isbn = "978-3-030-24257-2",

volume = "11628",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "136--154",

editor = "\{Mikol{\'a}{\v s} Janota, In{\^e}s Lynce\}",

booktitle = "Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19)",

}

Incremental Inprocessing SAT Solving. / Fazekas, Katalin; Biere, Armin; Scholl, Christoph.
Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19). ed. / Mikoláš Janota, Inês Lynce. Vol. 11628 Springer, 2019. p. 136-154 (Lecture Notes in Computer Science (LNCS)).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - Incremental Inprocessing SAT Solving

AU - Fazekas, Katalin

AU - Biere, Armin

AU - Scholl, Christoph

PY - 2019/7

Y1 - 2019/7

N2 - Incremental SAT is about solving a sequence of related SAT problems eﬃciently. It makes use of already learned information to avoid repeating redundant work. Also preprocessing and inprocessing are considered to be crucial. Our calculus uses the most general redundancy property and extends existing inprocessing rules to incremental SAT solving. It allows to automatically reverse earlier simpliﬁcation steps, which are inconsistent with literals in new incrementally added clauses. Our approach to incremental SAT solving not only simpliﬁes the use of inprocessing but also substantially improves solving time.

AB - Incremental SAT is about solving a sequence of related SAT problems eﬃciently. It makes use of already learned information to avoid repeating redundant work. Also preprocessing and inprocessing are considered to be crucial. Our calculus uses the most general redundancy property and extends existing inprocessing rules to incremental SAT solving. It allows to automatically reverse earlier simpliﬁcation steps, which are inconsistent with literals in new incrementally added clauses. Our approach to incremental SAT solving not only simpliﬁes the use of inprocessing but also substantially improves solving time.

M3 - Conference proceedings

SN - 978-3-030-24257-2

VL - 11628

T3 - Lecture Notes in Computer Science (LNCS)

SP - 136

EP - 154

BT - Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19)

A2 - Mikoláš Janota, Inês Lynce, null

PB - Springer

ER -