Reasoning with finite sets and cardinality constraints in SMT
From MaRDI portal
Publication:4553283
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
- scientific article; zbMATH DE number 1641581 (Why is no real title available?)
- scientific article; zbMATH DE number 3976287 (Why is no real title available?)
- scientific article; zbMATH DE number 2013582 (Why is no real title available?)
- scientific article; zbMATH DE number 1507186 (Why is no real title available?)
- scientific article; zbMATH DE number 2086594 (Why is no real title available?)
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
- A decision procedure for sets, binary relations and partial functions
- A polite non-disjoint combination method: theories with bridging functions revisited
- Combining sets with cardinals
- Counting constraints in flat array fragments
- Deciding Boolean algebra with Presburger arithmetic
- Decision Procedures for Multisets with Cardinality Constraints
- Decision procedures for theories of sets with measures
- Locality Results for Certain Extensions of Theories with Bridging Functions
- Polite theories revisited
- Sets with cardinality constraints in satisfiability modulo theories
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Term Rewriting and All That
- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
Cited in
(15)- Solving quantifier-free first-order constraints over finite sets and binary relations
- Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
- Tight representation of logical constraints as cardinality rules
- Polynomial Constraints for Sets with Cardinality Bounds
- 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
- Cardinal: a finite sets constraint solver
- Decision Procedures for Multisets with Cardinality Constraints
- On the convexity of a fragment of pure set theory with applications within a Nelson-Oppen framework
- scientific article; zbMATH DE number 1863393 (Why is no real title available?)
- MUNCH -- automated reasoner for sets and multisets
- Non-classical logics in satisfiability modulo theories
- Combining sets with cardinals
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)
