Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
From MaRDI portal
Publication:3608775
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
(32)- Cardinality constraints for arrays (decidability results and applications)
- One-variable logic meets Presburger arithmetic
- NP satisfiability for arrays as powers
- scientific article; zbMATH DE number 1696820 (Why is no real title available?)
- Counting constraints in flat array fragments
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Colors Make Theories Hard
- Decision procedures for region logic
- Sets with cardinality constraints in satisfiability modulo theories
- Linear Arithmetic with Stars
- 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
- The support of integer optimal solutions
- scientific article; zbMATH DE number 1903342 (Why is no real title available?)
- scientific article; zbMATH DE number 2090309 (Why is no real title available?)
- Certified reasoning with infinity
- Computer Aided Verification
- Automated Deduction – CADE-20
- Decision Procedures for Multisets with Cardinality Constraints
- On algebraic array theories
- How to tell easy from hard: complexities of conjunctive query entailment in extensions of \(\mathcal{ALC}\)
- Succinct ordering and aggregation constraints in algebraic array theories
- Two variable logic with ultimately periodic counting
- Polite combination in parametric array theories
- Deciding satisfiability for overlaid symbolic heaps
- The expressive power of description logics with numerical constraints over restricted classes of models
- Concrete domains meet expressive cardinality restrictions in description logics
- New support size bounds for integer programming, applied to makespan minimization on uniformly related machines
- On the complexity of convex and reverse convex prequadratic constraints
- On homogeneous models of fluted languages
- Deciding Boolean algebra with Presburger arithmetic
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)
