A Computing Procedure for Quantification Theory

Cites work

A comparative runtime analysis of heuristic algorithms for satisfiability problems
A Computing Procedure for Quantification Theory
An improved exponential-time algorithm for k -SAT
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?)
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)

A generative power-law search tree model
Learning action models from plan examples using weighted MAX-SAT
Resolution for Max-SAT
Labelled splitting
\texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver
First order Stålmarck. Universal lemmas through branch merges
Theory decision by decomposition
Automated theorem proving methods
Condensed detachment as a rule of inference
Efficient algorithms for combinatorial problems on graphs with bounded decomposability - a survey
The intractability of resolution
Polynomial-average-time satisfiability problems
Resolution vs. cutting plane solution of inference problems: Some computational experience
Inconsistency check of a set of clauses using Petri net reductions
Some results and experiments in programming techniques for propositional logic
A parallel approach for theorem proving in propositional logic
A satisfiability tester for non-clausal propositional calculus
Probabilistic performance of a heurisic for the satisfiability problem
Stratification and knowledge base management
Logic applied to integer programming and integer programming applied to logic
Backtracking with multi-level dynamic search rearrangement
A switching algorithm for the solution of quadratic Boolean equations
Solving the satisfiability problem by using randomized approach
Tseitin's formulas revisited
Complexity of resolution proofs and function introduction
An efficient algorithm for the 3-satisfiability problem
Graph properties for normal logic programs
On the role of unification in mechanical theorem proving
On the complexity of regular resolution and the Davis-Putnam procedure
Prolog technology for default reasoning: proof theory and compilation techniques
Linear programs for constraint satisfaction problems
How good are branching rules in DPLL?
Length of prime implicants and number of solutions of random CNF formulae
A two-phase algorithm for solving a class of hard satisfiability problems
Simplification in a satisfiability checker for VLSI applications
An exact algorithm for the constraint satisfaction problem: Application to logical inference
Inference flexibility in Horn clause knowledge bases and the simplex method
A kind of logical compilation for knowledge bases
Tractability through symmetries in propositional calculus
Problem solving by searching for models with a theorem prover
On problems with short certificates
Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
Minimization of a quadratic pseudo-Boolean function
Easy problems are sometimes hard
Ordered model trees: A normal form for disjunctive deductive databases
Embedding complex decision procedures inside an interactive theorem prover.
Davis-Putnam resolution versus unrestricted resolution
An average case analysis of a resolution principle algorithm in mechanical theorem proving.
Branch-and-cut solution of inference problems in propositional logic
Solving propositional satisfiability problems
Disjunctive stable models: Unfounded sets, fixpoint semantics, and computation
A BDD SAT solver for satisfiability testing: An industrial case study
A fast parallel SAT-solver -- efficient workload balancing
Local and global relational consistency
Resolution lower bounds for the weak functional pigeonhole principle.
Approximating minimal unsatisfiable subformulae by means of adaptive core search
How to fake an RSA signature by encoding modular root finding as a SAT problem
Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT.
Worst-case study of local search for MAX-\(k\)-SAT.
On the structure of some classes of minimal unsatisfiable formulas
Equivalent literal propagation in the DLL procedure
A satisfiability procedure for quantified Boolean formulae
Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors.
Relative efficiency of propositional proof systems: Resolution vs. cut-free LK
Complexity-theoretic models of phase transitions in search problems
Alternative foundations for Reiter's default logic
Backtracking tactics in the backtrack method for SAT
Proving unsatisfiability of CNFs locally
An algorithm based on tabu search for satisfiability problem
A note about k-DNF resolution
P\(_-\)UNSAT approach of attractor calculation for Boolean gene regulatory networks
Relating size and width in variants of Q-resolution
Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms
Efficient, verified checking of propositional proofs
Semantically-guided goal-sensitive reasoning: inference system and completeness
Cliques enumeration and tree-like resolution proofs
A complexity dichotomy for matching cut in (bipartite) graphs of fixed diameter
On semantic cutting planes with very small coefficients
Conflict-driven answer set solving: from theory to practice
Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable
Counting models for 2SAT and 3SAT formulae
Resolution cannot polynomially simulate compressed-BFS
On SAT instance classes and a method for reliable performance experiments with SAT solvers
Efficient data structures for backtrack search SAT solvers
Toward leaner binary-clause reasoning in a satisfiability solver
A complete adaptive algorithm for propositional satisfiability
Boolean unification - the story so far
The linked conjunct method for automatic deduction and related search techniques
On the relations between SAT and CSP enumerative algorithms
Solving satisfiability problems using elliptic approximations -- effective branching rules
Partitioning methods for satisfiability testing on large formulas
Tractable reasoning via approximation
Reasoning, nonmonotonicity and learning in connectionist networks that capture propositional knowledge
Complete on average Boolean satisfiability
Improved exact algorithms for MAX-SAT
On the automatizability of resolution and related propositional proof systems
A sharp threshold in proof complexity yields lower bounds for satisfiability search
Branching rules for satisfiability
Propositional truth maintenance systems: Classification and complexity analysis
Structured proof procedures

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)