Solving non-linear arithmetic
From MaRDI portal
Recommendations
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Solving nonlinear integer arithmetic with MCSAT
- A CDCL-style calculus for solving non-linear constraints
- A search-based procedure for nonlinear real arithmetic
- SAT modulo linear arithmetic for solving polynomial constraints
Cited in
(84)- raSAT: an SMT solver for polynomial constraints
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Using machine learning to improve cylindrical algebraic decomposition
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- A CDCL-style calculus for solving non-linear constraints
- Counterexample- and simulation-guided floating-point loop invariant synthesis
- Learning modulo theories for constructive preference elicitation
- A conflict-driven solving procedure for poly-power constraints
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Editorial: Symbolic computation and satisfiability checking
- Fully incremental cylindrical algebraic decomposition
- Cylindrical algebraic decomposition with equational constraints
- From simplification to a partial theory solver for non-linear real polynomial constraints
- Applying computer algebra systems with SAT solvers to the Williamson conjecture
- A non-linear arithmetic procedure for control-command software verification
- Constructing a single cell in cylindrical algebraic decomposition
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Automated analysis of cryptographic assumptions in generic group models
- Deniable Functional Encryption
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- raSAT: An SMT Solver for Polynomial Constraints
- Speeding up the constraint-based method in difference logic
- Quantitative abstractions for collective adaptive systems
- Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- A survey of satisfiability modulo theory
- Semantically-guided goal-sensitive reasoning: model representation
- Solving nonlinear integer arithmetic with MCSAT
- Adapting real quantifier elimination methods for conflict set computation
- Satisfiability of non-linear (ir)rational arithmetic
- Satisfiability modulo theories
- Are parametric Markov chains monotonic?
- Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
- Sequential convex programming for the efficient verification of parametric MDPs
- scientific article; zbMATH DE number 5116531 (Why is no real title available?)
- Recent advances in real geometric reasoning
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- SAT modulo linear arithmetic for solving polynomial constraints
- Satisfiability checking: theory and applications
- Deciding floating-point logic with abstract conflict driven clause learning
- A symbiosis of interval constraint propagation and cylindrical algebraic decomposition
- Incomplete SMT techniques for solving non-linear formulas over the integers
- Improved Cross-Validation for Classifiers that Make Algorithmic Choices to Minimise Runtime Without Compromising Output Correctness
- Solving non-linear Horn clauses using a linear Horn clause solver
- Barrier certificates revisited
- Structured learning modulo theories
- A search-based procedure for nonlinear real arithmetic
- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
- Computer Science Logic
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- scientific article; zbMATH DE number 2247681 (Why is no real title available?)
- Linear and nonlinear arithmetic in ACL2
- Symbolic computation of differential equivalences
- Truth table invariant cylindrical algebraic decomposition
- Cylindrical algebraic decomposition using local projections
- Verification Modulo theories
- Automated analysis of tethered DNA nanostructures using constraint solving
- Analysis and Transformation of Constrained Horn Clauses for Program Verification
- From Polynomial Invariants to Linear Loops
- An SMT solver for non-linear real arithmetic inside maple
- FOSSIL
- Explainable AI insights for symbolic computation: a case study on selecting the variable ordering for cylindrical algebraic decomposition
- Levelwise construction of a single cylindrical algebraic cell
- Computing with Tarski formulas and semi-algebraic sets in a web browser
- Verified Quadratic Virtual Substitution for Real Arithmetic
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Local search for solving satisfiability of polynomial formulas
- Satisfiability modulo finite fields
- Recent developments in real quantifier elimination and cylindrical algebraic decomposition (extended abstract of invited talk)
- More is less: adding polynomials for faster explanations in NLSAT
- Iterated resultants and rational functions in real quantifier elimination
- The CDSAT method for satisfiability modulo theories and assignment: an exposition
- The QSMA algorithm for quantifiers in SMT
- The geometry of cylindrical algebraic decomposition
- On the complexity of convex and reverse convex prequadratic constraints
- SMT solving over finite field arithmetic
- Generalized optimization modulo theories
- MCSat-based finite field reasoning in the \textsc{Yices2} SMT solver (short paper)
- Cutoff theorems for the equivalence of parameterized quantum circuits
- Breaking the data barrier in learning symbolic computation: a case study on variable ordering suggestion for cylindrical algebraic decomposition
- Learning probabilistic termination proofs
- Interpolation and model checking for nonlinear arithmetic
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
This page was built for publication: Solving non-linear arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2908506)
