Efficient Generation of Small Interpolants in CNF

DOI10.1007/978-3-642-39799-8_23MaRDI QIDQ2864838zbMATH OpenOpenAlexFDO

Authors Yakir Vizel, Vadim Ryvchin, Alexander Nadel

Publication date 26 November 2013

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-39799-8_23

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Efficient generation of small interpolants in CNF
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Efficient interpolant generation in satisfiability modulo linear integer arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Efficient CNF encoding of Boolean cardinality constraints
• Generalised interpolation by solving recursion-free Horn clauses
• On the Parameterized Complexity of Finding Small Unsatisfiable Subsets of CNF Formulas and CSP Instances
• Efficient CNF simplification based on binary implication graphs

Cited in

(4)

• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Efficient generation of small interpolants in CNF
• Optimization techniques for Craig interpolant compaction in unbounded model checking

This page was built for publication: Efficient Generation of Small Interpolants in CNF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2864838)