A machine program for theorem-proving
From MaRDI portal
Publication:5621961
DOI10.1145/368273.368557zbMath0217.54002OpenAlexW2057361103WikidataQ29399031 ScholiaQ29399031MaRDI QIDQ5621961
Donald W. Loveland, George Logemann, Martin Davis
Publication date: 1962
Published in: Communications of the ACM (Search for Journal in Brave)
Full work available at URL: http://hdl.handle.net/2027/mdp.39015095248095
Related Items
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, An experiment with satisfiability modulo SAT, Formalization and implementation of modern SAT solvers, A collaborative approach for multi-threaded SAT solving, SAT-solving in practice, with a tutorial example from supervisory control, An integer programming approach to the multimode resource-constrained multiproject scheduling problem, Substitutions into propositional tautologies, An approach using SAT solvers for the RCPSP with logical constraints, Density condensation of Boolean formulas, A competitive and cooperative approach to propositional satisfiability, Answer set programming based on propositional satisfiability, The SAT-based approach to separation logic, 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, The complexity of pure literal elimination, Symbolic techniques in satisfiability solving, Solving non-Boolean satisfiability problems with stochastic local search: A comparison of encodings, Stochastic enumeration method for counting NP-hard problems, Planning as satisfiability: heuristics, Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances, A weight-balanced branching rule for SAT, Fast congruence closure and extensions, An efficient approach to solving random \(k\)-SAT problems, Some computational aspects of DISTANCE SAT, Comparing instance generation methods for automated reasoning, The disconnection tableau calculus, Solving satisfiability problems with preferences, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, HySAT: An efficient proof engine for bounded model checking of hybrid systems, Optimization techniques for Craig interpolant compaction in unbounded model checking, A SAT-based preimage analysis of reduced \textsc{Keccak} hash functions, On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\), An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty, Decomposition representations of logical equations in problems of inversion of discrete functions, Towards NP-P via proof complexity and search, A numerical method for Lane-Emden equations using hybrid functions and the collocation method, Soundness of \(\mathcal{Q}\)-resolution with dependency schemes, Non existence of some mixed Moore graphs of diameter 2 using SAT, Finding kernels or solving SAT, Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models, A randomized algorithm for 3-SAT, Computing weighted solutions in ASP: representation-based method vs. search-based method, Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers, Learning from conflicts in propositional satisfiability, A pearl on SAT and SMT solving in Prolog, Model evolution with equality -- revised and implemented, Toward a model for backtracking and dynamic programming, Combining decision procedures by (model-)equality propagation, A note on SAT algorithms and proof complexity, On deciding satisfiability by theorem proving with speculative inferences, An instantiation scheme for satisfiability modulo theories, Explaining the \texttt{cumulative} propagator, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Automatic verification of reduction techniques in higher order logic, Scatter search and genetic algorithms for MAX-SAT problems, Bernstein series solution of a class of Lane-Emden type equations, Curriculum-based course timetabling with SAT and MaxSAT, Quantifier elimination by dependency sequents, Deciding floating-point logic with abstract conflict driven clause learning, An efficient solver for weighted Max-SAT, Matroid enumeration for incidence geometry, New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability, An overview of parallel SAT solving, Relating constraint answer set programming languages and algorithms, Finding rough and fuzzy-rough set reducts with SAT, CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability, Two approximate algorithms for model counting, Improving configuration checking for satisfiable random \(k\)-SAT instances, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, A search-based procedure for nonlinear real arithmetic, Exact algorithms for exact satisfiability and number of perfect matchings, New methods for proving the impossibility to solve problems through reduction of problem spaces, A logic-algebraic approach to decision taking in a railway interlocking system, Cardinality networks: a theoretical and empirical study, John McCarthy's legacy, On the power of clause-learning SAT solvers as resolution engines, Leveraging belief propagation, backtrack search, and statistics for model counting, 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, A generative power-law search tree model, A self-adaptive multi-engine solver for quantified Boolean formulas, An approach for extracting a small unsatisfiable core, Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT, A rigorous methodology for specification and verification of business processes, Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems, \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver, Data compression for proof replay, Average time analyses of simplified Davis-Putnam procedures, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Improving exact algorithms for MAX-2-SAT, A parallelization scheme based on work stealing for a class of SAT solvers, On market-inspired approaches to propositional satisfiability, Backjumping for quantified Boolean logic satisfiability, SAT-based planning in complex domains: Concurrency, constraints and nondeterminism, Contingent planning under uncertainty via stochastic satisfiability, Configuration landscape analysis and backbone guided local search. I: Satisfiability and maximum satisfiability, On preprocessing techniques and their impact on propositional model counting, Gearing Up for Effective ASP Planning, Algorithms for Solving Satisfiability Problems with Qualitative Preferences, Group classification of a generalized Lane-Emden system, What we can learn from conflicts in propositional satisfiability, A unified framework for DPLL(T) + certificates, A Groebner bases-based approach to backward reasoning in rule based expert systems, New upper bound for the \#3-SAT problem, Backdoors to Satisfaction, Local-search extraction of mUSes, Exploiting multivalued knowledge in variable selection heuristics for SAT solvers, A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic, Generalizing DPLL and satisfiability for equalities, The state of SAT, BerkMin: A fast and robust SAT-solver, Conflict-directed \(A^{*}\) and its role in model-based embedded systems, Random backtracking in backtrack search algorithms for satisfiability, Regular-SAT: A many-valued approach to solving combinatorial problems, A logical approach to efficient Max-SAT solving, The model evolution calculus as a first-order DPLL method, Solving quantified constraint satisfaction problems, On probabilistic inference by weighted model counting, Treewidth computation and extremal combinatorics, Conformant planning as a case study of incremental QBF solving, Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Anytime Computation of Cautious Consequences in Answer Set Programming, Strong ETH and resolution via games and the multiplicity of strategies, Space Complexity in Polynomial Calculus, On First-Order Model-Based Reasoning, Generating hard satisfiability problems, Experimental results on the crossover point in random 3-SAT, The satisfiability constraint gap, Some pitfalls for experimenters with random SAT, Hard random 3-SAT problems and the Davis-Putnam procedure, Long-distance Q-resolution with dependency schemes, Portfolios in stochastic local search: efficiently computing most probable explanations in Bayesian networks, An Expressive Model for Instance Decomposition Based Parallel SAT Solvers, 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, An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, Satisfiability in composition-nominative logics, Search techniques for SAT-based Boolean optimization, Conformant planning via heuristic forward search: A new approach, Processes and continuous change in a SAT-based planner, MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability, Partition-based logical reasoning for first-order and propositional theories, Compiling problem specifications into SAT, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, A SAT-based parser and completer for pictures specified by tiling, Visualizing SAT instances and runs of the DPLL algorithm, Optimizing terminological reasoning for expressive description logics, How to Apply SAT-Solving for the Equivalence Test of Monotone Normal Forms, Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One, Generalized Conflict-Clause Strengthening for Satisfiability Solvers, Empirical Study of the Anatomy of Modern Sat Solvers, Generalised graph colouring by a hybrid of local search and constraint programming, Another look at graph coloring via propositional satisfiability, Conflict analysis in mixed integer programming, Algorithms for computing minimal unsatisfiable subsets of constraints, Extended resolution simulates binary decision diagrams, GridSAT: Design and implementation of a computational grid application, Exact Max-SAT solvers for over-constrained problems, Embedded software verification using symbolic execution and uninterpreted functions, Selection of search strategies for solving 3-SAT problems, $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation, Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space, A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality, Tight Upper Bound on Splitting by Linear Combinations for Pigeonhole Principle, On the Hardness of SAT with Community Structure, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, Incremental Determinization, Long Distance Q-Resolution with Dependency Schemes, Transition systems for model generators—A unifying approach, $$P\mathop{ =}\limits^{?}NP$$, A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic, Opposition Frameworks, DRAT Proofs for XOR Reasoning, Beweisalgorithmen für die Prädikatenlogik, Hard satisfiable instances for DPLL-type algorithms, The resolution complexity of random graph \(k\)-colorability, Typical case complexity of satisfiability algorithms and the threshold phenomenon, Bounded Model Checking with Parametric Data Structures, Interpolant Learning and Reuse in SAT-Based Model Checking, Encoding First Order Proofs in SMT, Formal verification of a generic framework to synthesize SAT-provers, Distributing the Workload in a Lazy Theorem-Prover, Automated formal analysis and verification: an overview, Cutting to the chase., SMELS: satisfiability modulo equality with lazy superposition, Machine learning for first-order theorem proving, Complete on average Boolean satisfiability, Nagging: A scalable fault-tolerant paradigm for distributed search, Automated generation of exam sheets for automated deduction, On the automatizability of resolution and related propositional proof systems, A sharp threshold in proof complexity yields lower bounds for satisfiability search, A note about \(k\)-DNF resolution, P\(_-\)UNSAT approach of attractor calculation for Boolean gene regulatory networks, An average case analysis of a resolution principle algorithm in mechanical theorem proving., A parallel approach for theorem proving in propositional logic, An exponential lower bound for the pure literal rule, Satisfiability modulo theory (SMT) formulation for optimal scheduling of task graphs with communication delay, Relating size and width in variants of Q-resolution, A logic-based Benders decomposition for microscopic railway timetable planning, A verified SAT solver framework with learn, forget, restart, and incrementality, What convex geometries tell about shattering-extremal systems, A BDD SAT solver for satisfiability testing: An industrial case study, Structured proof procedures, Three-valued semantics for hybrid MKNF knowledge bases revisited, Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms, Efficient, verified checking of propositional proofs, Reconstructing \((h,v)\)-convex \(2\)-dimensional patterns of objects from approximate horizontal and vertical projections., What is answer set programming to propositional satisfiability, 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., Resolution and binary decision diagrams cannot simulate each other polynomially, 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, On the limit of branching rules for hard random unsatisfiable 3-SAT, A satisfiability procedure for quantified Boolean formulae, SAT problems with chains of dependent variables, The complexity of inverting explicit Goldreich's function by DPLL algorithms, Semantically-guided goal-sensitive reasoning: inference system and completeness, A coupled method of Laplace transform and Legendre wavelets for Lane-Emden-type differential equations, Cliques enumeration and tree-like resolution proofs, Formal verification based on Boolean expression diagrams, First-order automated reasoning with theories: when deduction modulo theory meets practice, New methods for 3-SAT decision and worst-case analysis, The \(Multi\)-SAT algorithm, Complexity analysis of propositional resolution with autarky pruning, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Solving SAT by algorithm transform of Wu's method, Mind the gap -- a closer look at the security of block ciphers against differential cryptanalysis, Faradžev Read-type enumeration of non-isomorphic CC systems, Improved algorithms for the general exact satisfiability problem, On the complexity of choosing the branching literal in DPLL, Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions, On semantic cutting planes with very small coefficients, Programming for modular reconfigurable robots, Resource-constrained project scheduling with activity splitting and setup times, Conflict-driven answer set solving: from theory to practice, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Accelerating backtrack search with a best-first-search strategy, Resolution cannot polynomially simulate compressed-BFS, Limitations of restricted branching in clause learning, Propagation via lazy clause generation, On SAT instance classes and a method for reliable performance experiments with SAT solvers, Testing satisfiability of CNF formulas by computing a stable set of points, Efficient data structures for backtrack search SAT solvers, Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT, Toward leaner binary-clause reasoning in a satisfiability solver, Characterising tree-like Frege proofs for QBF, Reversible pebble games and the relation between tree-like and general resolution space, A conflict-driven solving procedure for poly-power constraints, A complete adaptive algorithm for propositional satisfiability, Inference approach based on Petri nets, Editorial: Symbolic computation and satisfiability checking, How good are branching rules in DPLL?, New complexity results for Łukasiewicz logic, 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, Formally verifying the solution to the Boolean Pythagorean triples problem, First order Stålmarck. Universal lemmas through branch merges, Theory decision by decomposition, Symmetric matroid polytopes and their generation, Hyperresolution for Gödel logic with truth constants, 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, Resolution over linear equations modulo two, Graph-based construction of minimal models, Equivalency reasoning to solve a class of hard SAT problems., A novel SAT solver for the van der Waerden numbers, Moderate exponential-time algorithms for scheduling problems, A two-phase algorithm for solving a class of hard satisfiability problems, Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\)., Partitioning methods for satisfiability testing on large formulas, Solving strong controllability of temporal problems with uncertainty using SMT, About the incremental validation of first-order stratified knowledge-based decision-support systems, SCL(EQ): SCL for first-order logic with equality, Accelerating logic-based benders decomposition for railway rescheduling by exploiting similarities in delays, Extending and implementing the stable model semantics, Backjump-based backtracking for constraint satisfaction problems, Proving unsatisfiability of CNFs locally, Deep cooperation of CDCL and local search for SAT, Characterizing Tseitin-formulas with short regular resolution refutations, Assessing progress in SAT solvers through the Lens of incremental SAT, Projection heuristics for binary branchings between sum and product, Logical cryptanalysis with WDSat, Characterizing Tseitin-Formulas with Short Regular Resolution Refutations, Set covering heuristics in a benders decomposition for railway timetabling, Machine learning and logic: a new frontier in artificial intelligence, Using answer set programming to deal with Boolean networks and attractor computation: application to gene regulatory networks of cells, Towards better heuristics for solving bounded model checking problems, Experiments with automated reasoning in the class, On the observable restrictions of limited consideration models: theory and application, 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, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Diversifying a parallel SAT solver with Bayesian moment matching, Advice complexity of adaptive priority algorithms, Constrained multi-tildes, Unnamed Item, Cost-bounded argumentation, An automated approach to the Collatz conjecture, SCL(EQ): SCL for first-order logic with equality, MAX SAT approximation beyond the limits of polynomial-time approximation, Rigorous results for random (\(2+p)\)-SAT, Results related to threshold phenomena research in satisfiability: Lower bounds, Parameterized Complexity of DPLL Search Procedures, Faster than classical quantum algorithm for dense formulas of exact satisfiability and occupation problems, GD-SAT model and crossover line, Modular Inference of Linear Types for Multiplicity-Annotated Arrows, Specification and Verification of Multi-Agent Systems, A SAT-Based Approach for Index Calculus on Binary Elliptic Curves, Automated Reasoning Building Blocks, Craig Interpolation in the Presence of Non-linear Constraints, Superposition Modulo Non-linear Arithmetic, Approximate Model Counting via Extension Rule, Laissez-Faire Caching for Parallel #SAT Solving, $$\#\exists $$ SAT: Projected Model Counting, Evaluating CDCL Variable Scoring Schemes, Binary Decision Diagrams, Propositional SAT Solving, Satisfiability Modulo Theories, History and Prospects for First-Order Automated Deduction, Finding similar/diverse solutions in answer set programming, Unsatisfiable Formulae of Gödel Logic with Truth Constants and $$\varDelta $$ Are Recursively Enumerable, Partitioning methods for satisfiability testing on large formulas, Satisfiability Checking: Theory and Applications, On black-box optimization in divide-and-conquer SAT solving, Ordered Binary Decision Diagrams and the Davis-Putnam procedure, On CDCL-Based Proof Systems with the Ordered Decision Strategy, Unnamed Item, A Generalized Framework for Conflict Analysis, Random Instances of W[2-Complete Problems: Thresholds, Complexity, and Algorithms], A Decision-Making Procedure for Resolution-Based SAT-Solvers, Computation of Renameable Horn Backdoors, SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions, Regular and General Resolution: An Improved Separation, Disjunctive answer set solvers via templates, Clingcon: The next generation, Constraint answer set solver EZCSP and why integration schemas matter, 3-Valued Circuit SAT for STE with Automatic Refinement, A View from the Engine Room: Computational Support for Symbolic Model Checking, Logic + control: On program construction and verification, Exploiting data dependencies in many-valued logics, Limitations of Restricted Branching in Clause Learning, Towards Robust CNF Encodings of Cardinality Constraints, Stochastic Satisfiability Modulo Theory: A Novel Technique for the Analysis of Probabilistic Hybrid Systems, Symbolic Execution as DPLL Modulo Theories, On the Relationship between Hybrid Probabilistic Logic Programs and Stochastic Satisfiability, SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems, Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting, Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic, Breaking Cycle Structure to Improve Lower Bound for Max-SAT, Practical Implementation of a Quantum Backtracking Algorithm, Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT, My Life as a Logician, Banishing Ultrafilters from Our Consciousness, DPLL: The Core of Modern Satisfiability Solvers, An Algorithm for Approximating the Satisfiability Problem of High-level Conditions, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, Multi-threaded ASP solving with clasp, The Strategy Challenge in SMT Solving, Constructing Bachmair-Ganzinger Models, The Relative Power of Semantics and Unification, Exact Algorithms for MAX-SAT, Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers, Linear-Time Algorithm for Quantum 2SAT, Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases, Compressing Propositional Refutations, The Mechanical Verification of a DPLL-Based Satisfiability Solver, An Upper Bound on the Space Complexity of Random Formulae in Resolution, A Decidable Class of Nested Iterated Schemata, Challenges in Constraint-Based Analysis of Hybrid Systems, A Unified Framework for Certificate and Compilation for QBF, The complexity of resolution refinements, The Complexity of Propositional Proofs, Cutting to the Chase Solving Linear Integer Arithmetic, Solving Systems of Linear Inequalities by Bound Propagation, Justifications for logic programs under answer set semantics, Guided Search and a Faster Deterministic Algorithm for 3-SAT, Solving NP-Complete Problems with Quantum Search, Unnamed Item, Computational Aspects of Quasi-Classical Entailment, Supercritical Space-Width Trade-offs for Resolution, An Exponential Lower Bound for Width-Restricted Clause Learning, Boundary Points and Resolution, Cardinality Networks and Their Applications, Dynamic Symmetry Breaking by Simulating Zykov Contraction, An empirical study of constraint logic programming and answer set programming solutions of combinatorial problems, Short Proofs Are Hard to Find, Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods, EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas, BDD-based decision procedures for the modal logic K ★, Random matrix model of adiabatic quantum computing, A practical integration of first-order reasoning and decision procedures, SATO: An efficient propositional prover, Unnamed Item, Taming the Complexity of Temporal Epistemic Reasoning, Putting ABox Updates into Action, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Combining Instance Generation and Resolution, Unnamed Item, Toward unification of exact and heuristic optimization methods, Unnamed Item, Proving Termination with (Boolean) Satisfaction, Abstract Answer Set Solvers, Present and Future of Practical SAT Solving, Reflections on Proof Complexity and Counting Principles
Uses Software
