Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

DOI10.1007/978-3-540-73595-3_15MaRDI QIDQ3608775zbMATHOpenAlexFDO

Authors Viktor Kuncak, Martin C. Rinard

Publication date 6 March 2009

Published in Automated Deduction – CADE-21 (Search for Journal in Brave)

Full work available at URL http://infoscience.epfl.ch/record/110254

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• Deciding Boolean algebra with Presburger arithmetic
• scientific article; zbMATH DE number 1903342
• scientific article; zbMATH DE number 2090309
• Computer Aided Verification
• Optimal satisfiability checking for arithmetic \(\mu\)-calculi
• scientific article; zbMATH DE number 1979549
• Automated Deduction – CADE-20
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• scientific article; zbMATH DE number 1696820
• Enrichments of Boolean algebras by Presburger predicates

Cited in

(25)

• The support of integer optimal solutions
• Decision Procedures for Multisets with Cardinality Constraints
• Automated Deduction – CADE-20
• Cardinality constraints for arrays (decidability results and applications)
• Sets with cardinality constraints in satisfiability modulo theories
• Two variable logic with ultimately periodic counting
• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Colors Make Theories Hard
• scientific article; zbMATH DE number 1903342 (Why is no real title available?)
• Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
• Combining theories with shared set operations
• Reasoning with finite sets and cardinality constraints in SMT
• scientific article; zbMATH DE number 2090309 (Why is no real title available?)
• Counting constraints in flat array fragments
• How to tell easy from hard: complexities of conjunctive query entailment in extensions of \(\mathcal{ALC}\)
• Decision procedures for region logic
• Computer Aided Verification
• NP satisfiability for arrays as powers
• scientific article; zbMATH DE number 1696820 (Why is no real title available?)
• One-variable logic meets Presburger arithmetic
• Linear Arithmetic with Stars
• Succinct ordering and aggregation constraints in algebraic array theories
• Certified reasoning with infinity
• On algebraic array theories
• Deciding Boolean algebra with Presburger arithmetic

Describes a project that uses

Uses Software

• SMT-LIB
• SPASS+T
• UCLID
• Jahob

This page was built for publication: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

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