Reasoning with finite sets and cardinality constraints in SMT
From MaRDI portal
Publication:4553283
DOI10.23638/LMCS-14(4:12)2018zbMATH Open1403.68044arXiv1702.06259MaRDI QIDQ4553283FDOQ4553283
Andrew Reynolds, Clark Barrett, Kshitij Bansal, Cesare Tinelli
Publication date: 2 November 2018
Full work available at URL: https://arxiv.org/abs/1702.06259
Recommendations
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Sets with cardinality constraints in satisfiability modulo theories
- Cardinal: a finite sets constraint solver
- Polynomial Constraints for Sets with Cardinality Bounds
- Constraint solving for finite model finding in SMT solvers
Cites Work
- Title not available (Why is that?)
- Solving SAT and SAT Modulo Theories
- Term Rewriting and All That
- Sets with Cardinality Constraints in Satisfiability Modulo Theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- Deciding Boolean algebra with Presburger arithmetic
- Polite Theories Revisited
- Locality Results for Certain Extensions of Theories with Bridging Functions
- Title not available (Why is that?)
- Decision Procedures for Multisets with Cardinality Constraints
- Title not available (Why is that?)
- Combining sets with cardinals
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Counting Constraints in Flat Array Fragments
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
- A Decision Procedure for Sets, Binary Relations and Partial Functions
- Decision procedures for theories of sets with measures
Cited In (7)
- Tight representation of logical constraints as cardinality rules
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- Title not available (Why is that?)
- Non-classical logics in satisfiability modulo theories
- Combining sets with cardinals
Uses Software
This page was built for publication: Reasoning with finite sets and cardinality constraints in SMT
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4553283)
