A Computing Procedure for Quantification Theory

From MaRDI portal

Publication:5613969

Jump to:navigation, search

DOI10.1145/321033.321034zbMath0212.34203OpenAlexW2062897452WikidataQ29030829 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

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

Related Items

Conditional term rewriting and first-order theorem proving, Characterizing Tseitin-Formulas with Short Regular Resolution Refutations, Modular Inference of Linear Types for Multiplicity-Annotated Arrows, NEURAL NETWORKS AND LINEAR PROGRAMMING FOR THE SATISFIABILITY PROBLEM, Seventy Years of Computer Science, History and Prospects for First-Order Automated Deduction, Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable, Improved MaxSAT Algorithms for Instances of Degree 3, Computational logic: its origins and applications, Partitioning methods for satisfiability testing on large formulas, Tautology Elimination, Cut Elimination, and S5, A Computing Procedure for Quantification Theory, Unnamed Item, Satisfiability Checking: Theory and Applications, Persistence and Herbrand expansions, 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, Mining definitions in Kissat with Kittens, Unnamed Item, The impact of heterogeneity and geometry on the proof complexity of random satisfiability, A formalised theorem in the partition calculus, Computation of Renameable Horn Backdoors, Improvements to Hybrid Incremental SAT Algorithms, Clingcon: The next generation, Unnamed Item, 3-Valued Circuit SAT for STE with Automatic Refinement, An artificial neural network satisfiability tester, Unnamed Item, Limitations of Restricted Branching in Clause Learning, Towards Robust CNF Encodings of Cardinality Constraints, Logical Compilation of Bayesian Networks with Discrete Variables, Struktursätze der Algebra und Kompliziertheit logischer Schemata. III Algebraische Theorien und Verallgemeinerungen, Quantified Constraints in Twenty Seventeen, Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting, Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic, Quantum hypergraph states, Une approche intentionnelle du calcul des implicants premiers et essentiels des fonctions booléennes, Reducing fuzzy answer set programming to model finding in fuzzy logics, Approximate reasoning with credible subsets, Finding the Hardest Formulas for Resolution, Multi-threaded ASP solving with clasp, The Strategy Challenge in SMT Solving, The Relative Power of Semantics and Unification, Exact Algorithms for MAX-SAT, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, A Term Rewriting Technique for Decision Graphs, An Automata View to Goal-Directed Methods, Linear-Time Algorithm for Quantum 2SAT, An enhanced rostering model for airline crews, The Mechanical Verification of a DPLL-Based Satisfiability Solver, Iterative state-space reduction for flexible computation, An Upper Bound on the Space Complexity of Random Formulae in Resolution, Unnamed Item, Challenges in Constraint-Based Analysis of Hybrid Systems, A lower bound on CNF encodings of the at-most-one constraint, The Complexity of Propositional Proofs, Rigorous results for random (\(2+p)\)-SAT, Results related to threshold phenomena research in satisfiability: Lower bounds, PRACTICAL INCONSISTENCY MANAGEMENT FOR CRITICAL-TASKS DECISION-SUPPORT SYSTEMS, Cutting to the Chase Solving Linear Integer Arithmetic, Guided Search and a Faster Deterministic Algorithm for 3-SAT, Solving NP-Complete Problems with Quantum Search, Unnamed Item, Parameterized Complexity of DPLL Search Procedures, The search efficiency of theorem proving strategies, Semantically guided first-order theorem proving using hyper-linking, Str∔ve and integers, SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation, Bibliography of Hilary Putnam’s Writings in Logic and Mathematics, Supercritical Space-Width Trade-offs for Resolution, Proof Complexity of Non-classical Logics, SYSTEMATIC VERSUS LOCAL SEARCH AND GA TECHNIQUES FOR INCREMENTAL SAT, Preface, 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, 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, BDD-based decision procedures for the modal logic K ★, The probabilistic analysis of a greedy satisfiability algorithm, A practical integration of first-order reasoning and decision procedures, Some applications of propositional logic to cellular automata, Unnamed Item, Putting ABox Updates into Action, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Combining Instance Generation and Resolution, Toward unification of exact and heuristic optimization methods, Unnamed Item, Present and Future of Practical SAT Solving, Faster than classical quantum algorithm for dense formulas of exact satisfiability and occupation problems, Unnamed Item, Representations of the language recognition problem for a theorem prover, Reflections on Proof Complexity and Counting Principles, SAT-Inspired Eliminations for Superposition, Explaining by evidence, 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, Specification and Verification of Multi-Agent Systems, ASP Solving for Expanding Universes, Gearing Up for Effective ASP Planning, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, Craig Interpolation in the Presence of Non-linear Constraints, Superposition Modulo Non-linear Arithmetic, Recognition of Nested Gates in CNF Formulas, Binary Decision Diagrams, Propositional SAT Solving, Satisfiability Modulo Theories, New upper bound for the \#3-SAT problem, Backdoors to Satisfaction, An Improved SAT Algorithm in Terms of Formula Length, Exploiting multivalued knowledge in variable selection heuristics for SAT solvers, Counting for satisfiability by inverting resolution, Generalizing DPLL and satisfiability for equalities, The state of SAT, Random backtracking in backtrack search algorithms for satisfiability, 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, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, What convex geometries tell about shattering-extremal systems, From matchings to independent sets, Strong ETH and resolution via games and the multiplicity of strategies, Small Resolution Proofs for QBF using Dependency Treewidth, Space Complexity in Polynomial Calculus, On First-Order Model-Based Reasoning, Algorithms Solving the Matching Cut Problem, Modular strategic SMT solving with \textbf{SMT-RAT}, 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, Large Induced Subgraphs via Triangulations and CMSO, Matching cut: kernelization, single-exponential time FPT, and exact exponential algorithms, 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, First-order automated reasoning with theories: when deduction modulo theory meets practice, An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, A characterization of tree-like resolution size, Boundary properties of the satisfiability problems, Practical Implementation of a Quantum Backtracking Algorithm, Conformant planning via heuristic forward search: A new approach, MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability, Compiling problem specifications into SAT, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, Improved algorithms for the general exact satisfiability problem, Visualizing SAT instances and runs of the DPLL algorithm, Optimizing terminological reasoning for expressive description logics, My Life as a Logician, Banishing Ultrafilters from Our Consciousness, What Is Essential Unification?, DPLL: The Core of Modern Satisfiability Solvers, 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, Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions, Conflict analysis in mixed integer programming, Algorithms for computing minimal unsatisfiable subsets of constraints, Bipartite bihypergraphs: a survey and new results, Limitations of restricted branching in clause learning, Characterising tree-like Frege proofs for QBF, Embedded software verification using symbolic execution and uninterpreted functions, Selection of search strategies for solving 3-SAT problems, A conflict-driven solving procedure for poly-power constraints, $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation, Definability for model counting, 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, Autonomous Resolution Based on DNA Strand Displacement, Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods, Theorem proving with variable-constrained resolution, Beweisalgorithmen für die Prädikatenlogik, Hyperresolution for Gödel logic with truth constants, Resolution over linear equations modulo two, Hard satisfiable instances for DPLL-type algorithms, Bounded Model Checking with Parametric Data Structures, Interpolant Learning and Reuse in SAT-Based Model Checking, Formal verification of a generic framework to synthesize SAT-provers, Cutting to the chase., SMELS: satisfiability modulo equality with lazy superposition, Machine learning for first-order theorem proving, 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, Complete on average Boolean satisfiability, An algorithm based on tabu search for satisfiability problem, A kind of logical compilation for knowledge bases, Improved exact algorithms for MAX-SAT, Tractability through symmetries in propositional calculus, On the automatizability of resolution and related propositional proof systems, 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, A sharp threshold in proof complexity yields lower bounds for satisfiability search, Minimization of a quadratic pseudo-Boolean function, Easy problems are sometimes hard, Ordered model trees: A normal form for disjunctive deductive databases, A note about \(k\)-DNF resolution, P\(_-\)UNSAT approach of attractor calculation for Boolean gene regulatory networks, 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, Branching rules for satisfiability, Relating size and width in variants of Q-resolution, 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, Propositional truth maintenance systems: Classification and complexity analysis, Structured proof procedures, Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms, Local and global relational consistency, Efficient, verified checking of propositional proofs, 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, The complexity of inverting explicit Goldreich's function by DPLL algorithms, Semantically-guided goal-sensitive reasoning: inference system and completeness, Cliques enumeration and tree-like resolution proofs, Formal verification based on Boolean expression diagrams, New methods for 3-SAT decision and worst-case analysis, The \(Multi\)-SAT algorithm, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Separating signs in the propositional satisfiability problem, On the complexity of choosing the branching literal in DPLL, A complexity dichotomy for matching cut in (bipartite) graphs of fixed diameter, Tseitin's formulas revisited, Complexity of resolution proofs and function introduction, Time-free solution to SAT problem by tissue P systems, On semantic cutting planes with very small coefficients, An efficient algorithm for the 3-satisfiability problem, Conflict-driven answer set solving: from theory to practice, Graph properties for normal logic programs, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Counting models for 2SAT and 3SAT formulae, On the role of unification in mechanical theorem proving, Accelerating backtrack search with a best-first-search strategy, 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 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, On the complexity of regular resolution and the Davis-Putnam procedure, Generating extended resolution proofs with a BDD-based SAT solver, A complete adaptive algorithm for propositional satisfiability, Inference approach based on Petri nets, Prolog technology for default reasoning: proof theory and compilation techniques, Linear programs for constraint satisfaction problems, Boolean unification - the story so far, How good are branching rules in DPLL?, Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search, Length of prime implicants and number of solutions of random CNF formulae, A new branch-and-filter exact algorithm for binary constraint satisfaction problems, Relative efficiency of propositional proof systems: Resolution vs. cut-free LK, The linked conjunct method for automatic deduction and related search techniques, Exact algorithms for counting 3-colorings of graphs, Bounded-depth Frege complexity of Tseitin formulas for all graphs, On the relations between SAT and CSP enumerative algorithms, Solving satisfiability problems using elliptic approximations -- effective branching rules, Complexity-theoretic models of phase transitions in search problems, Alternative foundations for Reiter's default logic, Moderate exponential-time algorithms for scheduling problems, A two-phase algorithm for solving a class of hard satisfiability problems, Partitioning methods for satisfiability testing on large formulas, Tractable reasoning via approximation, Reasoning, nonmonotonicity and learning in connectionist networks that capture propositional knowledge, Backtracking tactics in the backtrack method for SAT, 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, Simplification in a satisfiability checker for VLSI applications, SCL(EQ): SCL for first-order logic with equality, An exact algorithm for the constraint satisfaction problem: Application to logical inference, Tractability beyond \(\beta\)-acyclicity for conjunctive queries with negation and SAT, Inference flexibility in Horn clause knowledge bases and the simplex method, Proving unsatisfiability of CNFs locally, Davis and Putnam meet Henkin: solving DQBF with resolution, 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, An automated approach to the Collatz conjecture, SCL(EQ): SCL for first-order logic with equality, An improved upper bound for SAT, 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, 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, Polynomial-average-time satisfiability problems, Substitutions into propositional tautologies, 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, 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, A satisfiability tester for non-clausal propositional calculus, Stochastic enumeration method for counting NP-hard problems, Simulating circuit-level simplifications on CNF, Probabilistic performance of a heurisic for the satisfiability problem, Algorithms for four variants of the exact satisfiability problem, A weight-balanced branching rule for SAT, Fast congruence closure and extensions, Stratification and knowledge base management, The disconnection tableau calculus, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Defining answer classes using resolution refutation, Satisfiability of acyclic and almost acyclic CNF formulas, Logic applied to integer programming and integer programming applied to logic, A characteristic set method for solving Boolean equations and applications in cryptanalysis of stream ciphers, On Davis-Putnam reductions for minimally unsatisfiable clause-sets, Optimization techniques for Craig interpolant compaction in unbounded model checking, Backtracking with multi-level dynamic search rearrangement, Towards NP-P via proof complexity and search, Exact algorithms for dominating set, Algorithms solving the matching cut problem, Finding kernels or solving SAT, Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models, A switching algorithm for the solution of quadratic Boolean equations, 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, Completeness of resolution revisited, An incremental method for generating prime implicants/implicates, Projecting systems of linear inequalities with binary variables, Incremental preprocessing methods for use in BMC, Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k-satisfiability problem, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Probabilistic bounds and algorithms for the maximum satisfiability problem, Curriculum-based course timetabling with SAT and MaxSAT, Formula dissection: A parallel algorithm for constraint satisfaction, Quantifier elimination by dependency sequents, Bounded list injective homomorphism for comparative analysis of protein-protein interaction graphs, Matroid enumeration for incidence geometry, New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability, An overview of parallel SAT solving, Meta-resolution: An algorithmic formalisation, CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability, Solving the satisfiability problem by using randomized approach, Prominent classes of the most general subsumptive solutions of Boolean equations, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, Dealing with 4-variables by resolution: an improved MaxSAT algorithm, A continuous approach to inductive inference, Efficient branch-and-bound algorithms for weighted MAX-2-SAT, John McCarthy's legacy, Leveraging belief propagation, backtrack search, and statistics for model counting, Linearity and regularity with negation normal form, Engineering constraint solvers for automatic analysis of probabilistic hybrid automata, Thread-parallel integrated test pattern generator utilizing satisfiability analysis, Foundations of \(r\)-contiguous matching in negative selection for anomaly detection, Short propositional refutations for dense random 3CNF formulas, A generative power-law search tree model, 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, Learning action models from plan examples using weighted MAX-SAT, Resolution for Max-SAT, Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-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, Compact and efficient encodings for planning in factored state and action spaces with learned binarized neural network transition models, Automated theorem proving methods, Condensed detachment as a rule of inference, Efficient algorithms for combinatorial problems on graphs with bounded decomposability - a survey, Unrestricted vs restricted cut in a tableau method for Boolean circuits, A parallelization scheme based on work stealing for a class of SAT solvers, The intractability of resolution, Contingent planning under uncertainty via stochastic satisfiability, Enhancing disjunctive logic programming systems by SAT checkers, Group cancellation and resolution

Cites Work

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