A Computing Procedure for Quantification Theory

From MaRDI portal

Publication:5613969

Jump to:navigation, search

DOI10.1145/321033.321034zbMath0212.34203WikidataQ29030829 ScholiaQ29030829MaRDI QIDQ5613969

Hilary Putnam, Martin Davis

Publication date: 1960

Published in: Journal of the ACM (Search for Journal in Brave)

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

Mathematics Subject Classification ID

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Related Items

An artificial neural network satisfiability tester, Une approche intentionnelle du calcul des implicants premiers et essentiels des fonctions booléennes, Approximate reasoning with credible subsets, An Upper Bound on the Space Complexity of Random Formulae in Resolution, Unnamed Item, SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation, Preface, Unnamed Item, Unnamed Item, Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable, Computational logic: its origins and applications, Partitioning methods for satisfiability testing on large formulas, Tautology Elimination, Cut Elimination, and S5, Unnamed Item, Satisfiability Checking: Theory and Applications, Clingcon: The next generation, Linear-Time Algorithm for Quantum 2SAT, Representations of the language recognition problem for a theorem prover, Explaining by evidence, NEURAL NETWORKS AND LINEAR PROGRAMMING FOR THE SATISFIABILITY PROBLEM, Unnamed Item, Unnamed Item, Reducing fuzzy answer set programming to model finding in fuzzy logics, Multi-threaded ASP solving with clasp, The Strategy Challenge in SMT Solving, The Relative Power of Semantics and Unification, Exact Algorithms for MAX-SAT, PRACTICAL INCONSISTENCY MANAGEMENT FOR CRITICAL-TASKS DECISION-SUPPORT SYSTEMS, Unnamed Item, Unnamed Item, Reflections on Proof Complexity and Counting Principles, Modular Inference of Linear Types for Multiplicity-Annotated Arrows, Seventy Years of Computer Science, Propositional calculus problems in CHIP, Simplifying clausal satisfiability problems, Ordered Binary Decision Diagrams and the Davis-Putnam procedure, On CDCL-Based Proof Systems with the Ordered Decision Strategy, Quantified Constraints in Twenty Seventeen, Quantum hypergraph states, Finding the Hardest Formulas for Resolution, A Term Rewriting Technique for Decision Graphs, The Mechanical Verification of a DPLL-Based Satisfiability Solver, Challenges in Constraint-Based Analysis of Hybrid Systems, Cutting to the Chase Solving Linear Integer Arithmetic, The search efficiency of theorem proving strategies, Semantically guided first-order theorem proving using hyper-linking, Str∔ve and integers, Bibliography of Hilary Putnam’s Writings in Logic and Mathematics, Supercritical Space-Width Trade-offs for Resolution, Short Proofs Are Hard to Find, Exact or approximate inference in graphical models: why the choice is dictated by the treewidth, and how variable elimination can be exploited, A practical integration of first-order reasoning and decision procedures, Toward unification of exact and heuristic optimization methods, Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting, Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic, The Complexity of Propositional Proofs, Guided Search and a Faster Deterministic Algorithm for 3-SAT, Solving NP-Complete Problems with Quantum Search, The probabilistic analysis of a greedy satisfiability algorithm, Present and Future of Practical SAT Solving, A Computing Procedure for Quantification Theory, Persistence and Herbrand expansions, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, An Automata View to Goal-Directed Methods, An enhanced rostering model for airline crews, Iterative state-space reduction for flexible computation, A lower bound on CNF encodings of the at-most-one constraint, Rigorous results for random (\(2+p)\)-SAT, Results related to threshold phenomena research in satisfiability: Lower bounds, Parameterized Complexity of DPLL Search Procedures, Proof Complexity of Non-classical Logics, Faster than classical quantum algorithm for dense formulas of exact satisfiability and occupation problems, SAT-Inspired Eliminations for Superposition, Conditional term rewriting and first-order theorem proving, Characterizing Tseitin-Formulas with Short Regular Resolution Refutations, Mining definitions in Kissat with Kittens, The impact of heterogeneity and geometry on the proof complexity of random satisfiability, A formalised theorem in the partition calculus, History and Prospects for First-Order Automated Deduction, Improved MaxSAT Algorithms for Instances of Degree 3, Computation of Renameable Horn Backdoors, Improvements to Hybrid Incremental SAT Algorithms, 3-Valued Circuit SAT for STE with Automatic Refinement, Limitations of Restricted Branching in Clause Learning, Towards Robust CNF Encodings of Cardinality Constraints, Logical Compilation of Bayesian Networks with Discrete Variables, SYSTEMATIC VERSUS LOCAL SEARCH AND GA TECHNIQUES FOR INCREMENTAL SAT, Cardinality Networks and Their Applications, Dynamic Symmetry Breaking by Simulating Zykov Contraction, Beyond CNF: A Circuit-Based QBF Solver, Combined Decision Techniques for the Existential Theory of the Reals, An empirical study of constraint logic programming and answer set programming solutions of combinatorial problems, BDD-based decision procedures for the modal logic K ★, Some applications of propositional logic to cellular automata, Putting ABox Updates into Action, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Combining Instance Generation and Resolution, Unnamed Item, Struktursätze der Algebra und Kompliziertheit logischer Schemata. III Algebraische Theorien und Verallgemeinerungen, An automated approach to the Collatz conjecture, SCL(EQ): SCL for first-order logic with equality, Further improvements for SAT in terms of formula length, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Spatial state-action features for general games, Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution, Depth lower bounds in Stabbing Planes for combinatorial principles, Computer-aided constructions of commafree codes, Are hitting formulas hard for resolution?, CliSAT: a new exact algorithm for hard maximum clique problems, Advice complexity of adaptive priority algorithms, Improving SAT Solving Using Monte Carlo Tree Search-Based Clause Learning, Constrained multi-tildes, MaxMinMax problem and sparse equations over finite fields, Interpolation systems for ground proofs in automated deduction: a survey, Semantically-guided goal-sensitive reasoning: model representation, Stochastic enumeration method for counting NP-hard problems, Simulating circuit-level simplifications on CNF, Satisfiability of acyclic and almost acyclic CNF formulas, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, Towards NP-P via proof complexity and search, Exact algorithms for dominating set, Finding kernels or solving SAT, Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models, Toward a model for backtracking and dynamic programming, A note on SAT algorithms and proof complexity, On deciding satisfiability by theorem proving with speculative inferences, An instantiation scheme for satisfiability modulo theories, Dealing with satisfiability and \(n\)-ary CSPs in a logical framework, Incremental preprocessing methods for use in BMC, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Curriculum-based course timetabling with SAT and MaxSAT, Quantifier elimination by dependency sequents, An overview of parallel SAT solving, CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability, Prominent classes of the most general subsumptive solutions of Boolean equations, Dealing with 4-variables by resolution: an improved MaxSAT algorithm, Efficient branch-and-bound algorithms for weighted MAX-2-SAT, John McCarthy's legacy, Leveraging belief propagation, backtrack search, and statistics for model counting, Algorithms for four variants of the exact satisfiability problem, A weight-balanced branching rule for SAT, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, A characteristic set method for solving Boolean equations and applications in cryptanalysis of stream ciphers, Projecting systems of linear inequalities with binary variables, Matroid enumeration for incidence geometry, Meta-resolution: An algorithmic formalisation, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, A continuous approach to inductive inference, Linearity and regularity with negation normal form, Engineering constraint solvers for automatic analysis of probabilistic hybrid automata, Foundations of \(r\)-contiguous matching in negative selection for anomaly detection, Short propositional refutations for dense random 3CNF formulas, Efficient generation of small interpolants in CNF, A dual algorithm for the satisfiability problem, Negation in rule-based database languages: A survey, Negation by default and unstratifiable logic programs, Algorithms for the maximum satisfiability problem, Computational experience with an interior point algorithm on the satisfiability problem, Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT, Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models, Unrestricted vs restricted cut in a tableau method for Boolean circuits, A parallelization scheme based on work stealing for a class of SAT solvers, Contingent planning under uncertainty via stochastic satisfiability, Enhancing disjunctive logic programming systems by SAT checkers, Group cancellation and resolution, An improved upper bound for SAT, Proof complexity of modal resolution, A comparative runtime analysis of heuristic algorithms for satisfiability problems, Formalization and implementation of modern SAT solvers, SAT-solving in practice, with a tutorial example from supervisory control, Substitutions into propositional tautologies, Density condensation of Boolean formulas, Heuristic-based backtracking relaxation for propositional satisfiability, Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas, Backdoor sets for DLL subsolvers, Symbolic techniques in satisfiability solving, Fast congruence closure and extensions, The disconnection tableau calculus, Defining answer classes using resolution refutation, Optimization techniques for Craig interpolant compaction in unbounded model checking, Algorithms solving the matching cut problem, Completeness of resolution revisited, An incremental method for generating prime implicants/implicates, Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k-satisfiability problem, Probabilistic bounds and algorithms for the maximum satisfiability problem, Formula dissection: A parallel algorithm for constraint satisfaction, Bounded list injective homomorphism for comparative analysis of protein-protein interaction graphs, New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability, Thread-parallel integrated test pattern generator utilizing satisfiability analysis, 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, The complexity of inverting explicit Goldreich's function by DPLL algorithms, Formal verification based on Boolean expression diagrams, New methods for 3-SAT decision and worst-case analysis, The \(Multi\)-SAT algorithm, Separating signs in the propositional satisfiability problem, On the complexity of choosing the branching literal in DPLL, Time-free solution to SAT problem by tissue P systems, Accelerating backtrack search with a best-first-search strategy, A satisfiability and workload-based exact method for the resource constrained project scheduling problem with generalized precedence constraints, Reversible pebble games and the relation between tree-like and general resolution space, Generating extended resolution proofs with a BDD-based SAT solver, Inference approach based on Petri nets, Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search, A new branch-and-filter exact algorithm for binary constraint satisfaction problems, Exact algorithms for counting 3-colorings of graphs, Bounded-depth Frege complexity of Tseitin formulas for all graphs, Moderate exponential-time algorithms for scheduling problems, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, A posthumous contribution by Larry Wos: excerpts from an unpublished column, SCL(EQ): SCL for first-order logic with equality, Tractability beyond \(\beta\)-acyclicity for conjunctive queries with negation and SAT, Davis and Putnam meet Henkin: solving DQBF with resolution, Characterizing Tseitin-formulas with short regular resolution refutations, Assessing progress in SAT solvers through the Lens of incremental SAT, A fast algorithm for SAT in terms of formula length, What convex geometries tell about shattering-extremal systems, Matching cut: kernelization, single-exponential time FPT, and exact exponential algorithms, First-order automated reasoning with theories: when deduction modulo theory meets practice, Improved algorithms for the general exact satisfiability problem, Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions, Limitations of restricted branching in clause learning, Characterising tree-like Frege proofs for QBF, A conflict-driven solving procedure for poly-power constraints, Definability for model counting, Hyperresolution for Gödel logic with truth constants, Resolution over linear equations modulo two, Cutting to the chase., SMELS: satisfiability modulo equality with lazy superposition, Machine learning for first-order theorem proving, On preprocessing techniques and their impact on propositional model counting, Solution validation and extraction for QBF preprocessing, Symbolic integration of logic in MILP branch and bound methods for the synthesis of process networks, New upper bound for the \#3-SAT problem, Exploiting multivalued knowledge in variable selection heuristics for SAT solvers, Counting for satisfiability by inverting resolution, A logical approach to efficient Max-SAT solving, The model evolution calculus as a first-order DPLL method, Solving quantified constraint satisfaction problems, Treewidth computation and extremal combinatorics, From matchings to independent sets, Strong ETH and resolution via games and the multiplicity of strategies, Modular strategic SMT solving with \textbf{SMT-RAT}, Resolution and linear CNF formulas: improved \((n,3)\)-\textsc{MaxSAT} algorithms, Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks, A Boolean satisfiability approach to the resource-constrained project scheduling problem, Solving RCPSP/max by lazy clause generation, A taxonomy of exact methods for partial Max-SAT, Complete Boolean satisfiability solving algorithms based on local search, Complexity and algorithms for recognizing polar and monopolar graphs, A characterization of tree-like resolution size, Boundary properties of the satisfiability problems, Conformant planning via heuristic forward search: A new approach, MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability, Compiling problem specifications into SAT, Visualizing SAT instances and runs of the DPLL algorithm, Optimizing terminological reasoning for expressive description logics, Conflict analysis in mixed integer programming, Algorithms for computing minimal unsatisfiable subsets of constraints, Bipartite bihypergraphs: a survey and new results, Embedded software verification using symbolic execution and uninterpreted functions, Selection of search strategies for solving 3-SAT problems, Theorem proving with variable-constrained resolution, Beweisalgorithmen für die Prädikatenlogik, Hard satisfiable instances for DPLL-type algorithms, Formal verification of a generic framework to synthesize SAT-provers, Generalizing DPLL and satisfiability for equalities, The state of SAT, Random backtracking in backtrack search algorithms for satisfiability, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Generating hard satisfiability problems, The satisfiability constraint gap, Some pitfalls for experimenters with random SAT, Hard random 3-SAT problems and the Davis-Putnam procedure, Critical behavior in the computational cost of satisfiability testing, $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation, Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, Predicate Elimination for Preprocessing in First-Order Theorem Proving, Bounded Model Checking with Parametric Data Structures, Interpolant Learning and Reuse in SAT-Based Model Checking, Gearing Up for Effective ASP Planning, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, Backdoors to Satisfaction, Space Complexity in Polynomial Calculus, On First-Order Model-Based Reasoning, Algorithms Solving the Matching Cut Problem, Large Induced Subgraphs via Triangulations and CMSO, An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, Satisfiability of Acyclic and almost Acyclic CNF Formulas (II), Generalized Conflict-Clause Strengthening for Satisfiability Solvers, Empirical Study of the Anatomy of Modern Sat Solvers, Autonomous Resolution Based on DNA Strand Displacement, Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods, Specification and Verification of Multi-Agent Systems, Craig Interpolation in the Presence of Non-linear Constraints, Superposition Modulo Non-linear Arithmetic, Binary Decision Diagrams, Propositional SAT Solving, Satisfiability Modulo Theories, An Improved SAT Algorithm in Terms of Formula Length, Practical Implementation of a Quantum Backtracking Algorithm, My Life as a Logician, Banishing Ultrafilters from Our Consciousness, What Is Essential Unification?, DPLL: The Core of Modern Satisfiability Solvers, ASP Solving for Expanding Universes, Recognition of Nested Gates in CNF Formulas, Small Resolution Proofs for QBF using Dependency Treewidth

Cites Work

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Publication:5613969&oldid=30265236"