Katalin Fazekas, Armin Biere, Christoph scholl,
"Incremental Inprocessing SAT Solving"
, in Mikolá? Janota, Inês Lynce: Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19), Serie Lecture Notes in Computer Science (LNCS), Vol. 11628, Springer, Seite(n) 136-154, 7-2019, ISBN: 978-3-030-24257-2
Incremental Inprocessing SAT Solving
Sprache des Titels:
Proc. 22nd Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'19)
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.