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
Authors: Kshitij Bansal, Clark Barrett, Andrew Reynolds, 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, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- 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 (15)
- Solving quantifier-free first-order constraints over finite sets and binary relations
- Polynomial Constraints for Sets with Cardinality Bounds
- Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
- Tight representation of logical constraints as cardinality rules
- Relational constraint solving in SMT
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- Sets with cardinality constraints in satisfiability modulo theories
- A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
- Decision Procedures for Multisets with Cardinality Constraints
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- Cardinal: a finite sets constraint solver
- MUNCH -- automated reasoner for sets and multisets
- 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)
