Parametric quantified SAT solving

DOI10.1145/1837934.1837954MaRDI QIDQ2946524zbMATH OpenOpenAlexFDO

Authors Thomas Sturm, Christoph Zengler

Publication date 17 September 2015

Published in Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1837934.1837954

zbMATH Keywords

generalizationparameterspropositional logicQSATquantifier eliminationSAT

Mathematics Subject Classification ID

Classical propositional logic (03B05) Quantifier elimination, model completeness, and related topics (03C10) Logical aspects of Boolean algebras (03G05) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• A satisfiability procedure for quantified Boolean formulae
• scientific article; zbMATH DE number 1979551
• Software for quantifier elimination in propositional logic
• New Domains for Applied Quantifier Elimination
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories

Cites work

• Differential algebra for derivations with nontrivial commutation rules
• Differential invariants of a Lie group action: syzygies on a generating set
• Differential invariants of conformal and projective surfaces
• Generating differential invariants
• Higher order contact of submanifolds of homogeneous spaces
• scientific article; zbMATH DE number 3762913 (Why is no real title available?)
• scientific article; zbMATH DE number 45257 (Why is no real title available?)
• scientific article; zbMATH DE number 3490133 (Why is no real title available?)
• scientific article; zbMATH DE number 2038305 (Why is no real title available?)
• scientific article; zbMATH DE number 2142844 (Why is no real title available?)
• scientific article; zbMATH DE number 3015982 (Why is no real title available?)
• scientific article; zbMATH DE number 802623 (Why is no real title available?)
• Invariants différentiels d'un pseudogroupe de Lie. I
• Invariants différentiels d'un pseudogroupe de Lie. II
• Moving coframes. II: Regularization and theoretical foundations
• Projective-type differential invariants and geometric curve evolutions of KdV-type in flat homogeneous manifolds
• Rational invariants of a group action. Construction and rewriting
• Smooth and algebraic invariants of a group action: Local and global constructions

Cited in

(3)

• Solving QSAT in sublinear depth
• Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases
• Better answers to real questions

Describes a project that uses

Uses Software

• REDUCE
• DIFFALG
• REDLOG
• RSat
• AIDA

This page was built for publication: Parametric quantified SAT solving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946524)