Pages that link to "Item:Q3455223"
From MaRDI portal
The following pages link to Solving SAT and SAT Modulo Theories (Q3455223):
Displaying 50 items.
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description) (Q2104500) (← links)
- Reasoning about vectors using an SMT theory of sequences (Q2104504) (← links)
- Multi-agent pathfinding with continuous time (Q2124435) (← links)
- Protocol analysis with time (Q2152027) (← links)
- Improved algorithms for the general exact satisfiability problem (Q2232607) (← links)
- Syntax-guided quantifier instantiation (Q2233503) (← links)
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories (Q2234101) (← links)
- Incremental search for conflict and unit instances of quantified formulas with E-matching (Q2234102) (← links)
- Refutation-based synthesis in SMT (Q2280222) (← links)
- The SAT+CAS method for combinatorial search with applications to best matrices (Q2294574) (← links)
- A conflict-driven solving procedure for poly-power constraints (Q2303230) (← links)
- \textsc{OptiMathSAT}: a tool for optimization modulo theories (Q2303246) (← links)
- Conflict-driven satisfiability for theory combination: transition system and completeness (Q2303254) (← links)
- SPASS-SATT. A CDCL(LA) solver (Q2305409) (← links)
- SCL clause learning from simple models (Q2305416) (← links)
- From simplification to a partial theory solver for non-linear real polynomial constraints (Q2307623) (← links)
- A complete and terminating approach to linear integer solving (Q2307624) (← links)
- Wombit: a portfolio bit-vector solver using word-level propagation (Q2323450) (← links)
- Estimating the volume of solution space for satisfiability modulo linear real arithmetic (Q2345986) (← links)
- Iterative and core-guided maxsat solving: a survey and assessment (Q2348540) (← links)
- Cutting to the chase. (Q2351157) (← links)
- On interpolation in automated theorem proving (Q2352502) (← links)
- Abstract interpretation as automated deduction (Q2360874) (← links)
- Automatically proving termination and memory safety for programs with pointer arithmetic (Q2362494) (← links)
- Deciding unifiability and computing local unifiers in the description logic \(\mathcal{EL}\) without top constructor (Q2374390) (← links)
- A unified framework for DPLL(T) + certificates (Q2375732) (← links)
- Complete Boolean satisfiability solving algorithms based on local search (Q2434568) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Satisfiability in composition-nominative logics (Q2445092) (← links)
- Metalevel transformation of strategies (Q2667189) (← links)
- Range and Set Abstraction using SAT (Q2814098) (← links)
- A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
- A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT (Q2817912) (← links)
- Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers (Q2818010) (← links)
- Deciding Bit-Vector Formulas with mcSAT (Q2818018) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- Opposition Frameworks (Q2835871) (← links)
- Model-based Theory Combination (Q2864402) (← links)
- Encoding First Order Proofs in SMT (Q2864408) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- On First-Order Model-Based Reasoning (Q2945706) (← links)
- Optimization Modulo Theories with Linear Rational Costs (Q2946768) (← links)
- An Equation-Based Classical Logic (Q2947458) (← links)
- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation (Q2964455) (← links)
- Axiomatic Constraint Systems for Proof Search Modulo Theories (Q2964465) (← links)
- Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One (Q3007689) (← links)
- On Interpolation in Decision Procedures (Q3010355) (← links)
- I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra (Q3014943) (← links)
- Access Nets: Modeling Access to Physical Spaces (Q3075481) (← links)
- Transition systems for model generators—A unifying approach (Q3087449) (← links)