Variable and clause elimination for LTL satisfiability checking

DOI10.1007/S11786-015-0240-2MaRDI QIDQ748758zbMATH OpenOpenAlexFDO

Authors Martin Suda

Publication date 30 October 2015

Published in Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1306.5539

zbMATH Keywords

satisfiabilitylinear temporal logicpreprocessing

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Abstract: We study preprocessing techniques for clause normal forms of LTL formulas. Applying the mechanism of labelled clauses enables us to reinterpret LTL satisfiability as a set of purely propositional problems and thus to transfer simplification ideas from SAT to LTL. We demonstrate this by adapting variable and clause elimination, a very effective preprocessing technique used by modern SAT solvers. Our experiments confirm that even in the temporal setting substantial reductions in formula size and subsequent decrease of solver runtime can be achieved.

Recommendations

• Theory and Applications of Satisfiability Testing
• Accelerating LTL satisfiability checking by SAT solvers
• Constraint LTL satisfiability checking without automata
• An explicit transition system construction approach to LTL satisfiability checking
• \(\mathrm{LTL}_{f}\) satisfiability checking

Cites work

• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• scientific article; zbMATH DE number 1950255 (Why is no real title available?)
• scientific article; zbMATH DE number 910719 (Why is no real title available?)
• A PLTL-prover based on labelled superposition with partial model guidance
• Blocked clause elimination
• Clausal temporal resolution
• Labelled superposition for PLTL
• On the Relationship between  -automata and Temporal Logic Normal Forms
• Symbolic Implementation of Alternating Automata
• Temporal logic can be more expressive
• The complexity of propositional linear temporal logics
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(2)

• scientific article; zbMATH DE number 5158957 (Why is no real title available?)
• SAT-based explicit LTL reasoning and its application to satisfiability checking

Describes a project that uses

Uses Software

• MiniSat
• TRP++

This page was built for publication: Variable and clause elimination for LTL satisfiability checking

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