Reduction of resolution refutations and interpolants via subsumption

Roderick Bloem, Sharad Malik, Matthias Schlaipfer, Georg Weissenbacher

Research output: Chapter in Book/Report/Conference proceedingChapter

4 Scopus citations

Abstract

Propositional resolution proofs and interpolants derived from them are widely used in automated verification and circuit synthesis. There is a broad consensus that “small is beautiful”—small proofs and interpolants lead to concise abstractions in verification and compact designs in synthesis.Contemporary proof reduction techniques either minimise the proof during construction, or perform a post-hoc transformation of a given resolution proof. We focus on the latter class and present a subsumption-based proof reduction algorithm that extends existing singlepass analyses and relies on ameet-over-all-paths analysis to identify redundant resolution steps and clauses.We show that smaller refutations do not necessarily entail smaller interpolants, and use labelled interpolation systems to generalise our reduction approach to interpolants. Experimental results support the theoretical claims.

Original languageEnglish (US)
Title of host publicationHardware and Software
Subtitle of host publicationVerification and Testing - 10th International Haifa Verification Conference, HVC 2014, Proceedings
EditorsEran Yahav
PublisherSpringer Verlag
Pages188-203
Number of pages16
ISBN (Electronic)9783319133379
DOIs
StatePublished - 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8855
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Reduction of resolution refutations and interpolants via subsumption'. Together they form a unique fingerprint.

Cite this