Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

DOI10.1007/978-3-540-73595-3_15zbMath1213.03021OpenAlexW1607550340MaRDI QIDQ3608775

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

Related Items (16)

Decision Procedures for Region Logic ⋮ NP satisfiability for arrays as powers ⋮ The Support of Integer Optimal Solutions ⋮ Cardinality constraints for arrays (decidability results and applications) ⋮ Linear Arithmetic with Stars ⋮ On algebraic array theories ⋮ Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars ⋮ One-variable logic meets Presburger arithmetic ⋮ Unnamed Item ⋮ Decision Procedures for Multisets with Cardinality Constraints ⋮ Certified Reasoning with Infinity ⋮ Sets with Cardinality Constraints in Satisfiability Modulo Theories ⋮ Counting Constraints in Flat Array Fragments ⋮ A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT ⋮ Colors Make Theories Hard ⋮ Combining Theories with Shared Set Operations

Uses Software

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

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