Pages that link to "Item:Q3455223"
From MaRDI portal
The following pages link to Solving SAT and SAT Modulo Theories (Q3455223):
Displaying 50 items.
- On abstract modular inference systems and solvers (Q286083) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- An experiment with satisfiability modulo SAT (Q287334) (← links)
- Adding decision procedures to SMT solvers using axioms with triggers (Q287384) (← links)
- Rewriting modulo SMT and open system analysis (Q347384) (← links)
- Ordered completion for first-order logic programs on finite structures (Q420824) (← links)
- A pearl on SAT and SMT solving in Prolog (Q428887) (← links)
- Curriculum-based course timetabling with SAT and MaxSAT (Q475170) (← links)
- Solving constraint satisfaction problems with SAT modulo theories (Q487632) (← links)
- Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (Q487655) (← links)
- Relating constraint answer set programming languages and algorithms (Q490456) (← links)
- SMT-based model checking for recursive programs (Q518396) (← links)
- An efficient SMT solver for string constraints (Q518402) (← links)
- Cardinality networks: a theoretical and empirical study (Q538318) (← links)
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
- Producing and verifying extremely large propositional refutations (Q694550) (← links)
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata (Q710668) (← links)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic (Q831915) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- The ins and outs of first-order runtime verification (Q888417) (← links)
- Better answers to real questions (Q898260) (← links)
- Hard problems in max-algebra, control theory, hypergraphs and other areas (Q990130) (← links)
- Theory decision by decomposition (Q1041591) (← links)
- A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
- Solving linear optimization over arithmetic constraint formula (Q1675635) (← links)
- Three-valued semantics for hybrid MKNF knowledge bases revisited (Q1677437) (← links)
- A progression semantics for first-order logic programs (Q1680677) (← links)
- raSAT: an SMT solver for polynomial constraints (Q1688535) (← links)
- Cardinality constraints for arrays (decidability results and applications) (Q1688541) (← links)
- What is answer set programming to propositional satisfiability (Q1699519) (← links)
- Conflict-driven answer set solving: from theory to practice (Q1761291) (← links)
- Twenty years of rewriting logic (Q1931904) (← links)
- Superposition as a decision procedure for timed automata (Q1949086) (← links)
- Superposition decides the first-order logic fragment over ground theories (Q1949088) (← links)
- Synthesis of quantifier-free DNF sentences from inconsistent samples of strings with EF games and SAT (Q2003999) (← links)
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system (Q2022307) (← links)
- IPL: an integration property language for multi-model cyber-physical systems (Q2024345) (← links)
- Efficiently and effectively recognizing toricity of steady state varieties (Q2035620) (← links)
- On solving quantified bit-vector constraints using invertibility conditions (Q2050109) (← links)
- Algorithmic reduction of biological networks with multiple time scales (Q2051597) (← links)
- Efficient SAT-based proof search in intuitionistic propositional logic (Q2055856) (← links)
- A unifying splitting framework (Q2055869) (← links)
- Superposition with first-class booleans and inprocessing clausification (Q2055873) (← links)
- Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic (Q2058375) (← links)
- Solving bitvectors with MCSAT: explanations from bits and pieces (Q2096440) (← links)
- A decision procedure for string to code point conversion (Q2096448) (← links)
- A posthumous contribution by Larry Wos: excerpts from an unpublished column (Q2102925) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- SAT-based proof search in intermediate propositional logics (Q2104497) (← links)