A Computing Procedure for Quantification Theory
From MaRDI portal
(Redirected from Publication:5613969)
Cites work
- scientific article; zbMATH DE number 986986 (Why is no real title available?)
- scientific article; zbMATH DE number 437557 (Why is no real title available?)
- scientific article; zbMATH DE number 3680816 (Why is no real title available?)
- scientific article; zbMATH DE number 3639144 (Why is no real title available?)
- A Computing Procedure for Quantification Theory
- A comparative runtime analysis of heuristic algorithms for satisfiability problems
- An improved exponential-time algorithm for k -SAT
- Implementing the Davis-Putnam method
- Linear Upper Bounds for Random Walk on Small Density Random 3‐CNFs
- On smoothed \(k\)-CNF formulas and the \texttt{Walksat} algorithm
- Survey propagation: An algorithm for satisfiability
- The complexity of theorem-proving procedures
- UnitWalk: A new SAT solver that uses local search guided by unit clause elimination
Cited in
(only showing first 100 items - show all)- Representations of the language recognition problem for a theorem prover
- Negation by default and unstratifiable logic programs
- Toward leaner binary-clause reasoning in a satisfiability solver
- Combined Decision Techniques for the Existential Theory of the Reals
- Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks
- Tight upper bound on splitting by linear combinations for pigeonhole principle
- Further improvements for SAT in terms of formula length
- Partitioning methods for satisfiability testing on large formulas
- Local redundancy in SAT: generalizations of blocked clauses
- Propositional calculus problems in CHIP
- Matroid enumeration for incidence geometry
- Backtracking tactics in the backtrack method for SAT
- A term rewriting technique for decision graphs
- Banishing ultrafilters from our consciousness
- What is essential unification?
- Tseitin's formulas revisited
- Partitioning methods for satisfiability testing on large formulas
- Algorithms Solving the Matching Cut Problem
- New methods for 3-SAT decision and worst-case analysis
- A continuous approach to inductive inference
- A switching algorithm for the solution of quadratic Boolean equations
- On the complexity of regular resolution and the Davis-Putnam procedure
- PRACTICAL INCONSISTENCY MANAGEMENT FOR CRITICAL-TASKS DECISION-SUPPORT SYSTEMS
- Characterizing Tseitin-formulas with short regular resolution refutations
- Efficient branch-and-bound algorithms for weighted MAX-2-SAT
- Local and global relational consistency
- Reflections on Proof Complexity and Counting Principles
- Computational experience with an interior point algorithm on the satisfiability problem
- A posthumous contribution by Larry Wos: excerpts from an unpublished column
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- SCL(EQ): SCL for first-order logic with equality
- Exact or approximate inference in graphical models: why the choice is dictated by the treewidth, and how variable elimination can be exploited
- Proof complexity of modal resolution
- Generating hard satisfiability problems
- Conformant planning via heuristic forward search: A new approach
- A satisfiability tester for non-clausal propositional calculus
- MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
- Symbolic techniques in satisfiability solving
- Compiling problem specifications into SAT
- Time-free solution to SAT problem by tissue P systems
- Fast congruence closure and extensions
- Accelerating backtrack search with a best-first-search strategy
- New upper bound for the \#3-SAT problem
- Depth lower bounds in Stabbing Planes for combinatorial principles
- DPLL: the core of modern satisfiability solvers
- Polynomial-average-time satisfiability problems
- Inconsistency check of a set of clauses using Petri net reductions
- On CDCL-Based Proof Systems with the Ordered Decision Strategy
- SCL(EQ): SCL for first-order logic with equality
- On the complexity of choosing the branching literal in DPLL
- Modular inference of linear types for multiplicity-annotated arrows
- Challenges in Constraint-Based Analysis of Hybrid Systems
- A new approach on solving 3-satisfiability
- The ghosts of forgotten things: a study on size after forgetting
- Generalized conflict-clause strengthening for satisfiability solvers
- Empirical study of the anatomy of modern SAT solvers
- Graph properties for normal logic programs
- Towards NP-P via proof complexity and search
- Exact algorithms for dominating set
- Machine learning for first-order theorem proving
- Linear-Time Algorithm for Quantum 2SAT
- A taxonomy of exact methods for partial Max-SAT
- The state of SAT
- Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
- On the structure of some classes of minimal unsatisfiable formulas
- Generalizing DPLL and satisfiability for equalities
- Tractability beyond -acyclicity for conjunctive queries with negation and SAT
- Tractability through symmetries in propositional calculus
- A comparative runtime analysis of heuristic algorithms for satisfiability problems
- Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic
- An automata view to goal-directed methods
- SatEx: A web-based framework for SAT experimentation
- John McCarthy's legacy
- A parallelization scheme based on work stealing for a class of SAT solvers
- On preprocessing techniques and their impact on propositional model counting
- The Complexity of Propositional Proofs
- Proving unsatisfiability of CNFs locally
- Computation of Renameable Horn Backdoors
- Multi-threaded ASP solving with clasp
- Satisfiability of acyclic and almost acyclic CNF formulas
- Bipartite bihypergraphs: a survey and new results
- Equivalent literal propagation in the DLL procedure
- Finding kernels or solving SAT
- A complexity dichotomy for matching cut in (bipartite) graphs of fixed diameter
- Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models
- Engineering constraint solvers for automatic analysis of probabilistic hybrid automata
- Reasoning, nonmonotonicity and learning in connectionist networks that capture propositional knowledge
- First order Stålmarck. Universal lemmas through branch merges
- A fast algorithm for SAT in terms of formula length
- Davis and Putnam meet Henkin: solving DQBF with resolution
- Linear programs for constraint satisfaction problems
- Substitutions into propositional tautologies
- Linearity and regularity with negation normal form
- The impact of heterogeneity and geometry on the proof complexity of random satisfiability
- Propositional truth maintenance systems: Classification and complexity analysis
- Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
- Limitations of restricted branching in clause learning
- MaxMinMax problem and sparse equations over finite fields
- The satisfiability constraint gap
This page was built for publication: A Computing Procedure for Quantification Theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5613969)
