The complexity of theorem-proving procedures
From MaRDI portal
Publication:5667480
DOI10.1145/800157.805047zbMath0253.68020OpenAlexW2036265926WikidataQ55867257 ScholiaQ55867257MaRDI QIDQ5667480
Publication date: 1971
Full work available at URL: https://doi.org/10.1145/800157.805047
Related Items
An easily testable optimal-time VLSI-multiplier ⋮ Heuristic evaluation techniques for bin packing approximation algorithms ⋮ A comment on \('NP=P?'\) and restricted partitions ⋮ NP-completeness results concerning greedy and super greedy linear extensions ⋮ An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines ⋮ Short propositional formulas represent nondeterministic computations ⋮ A comparison of polynomial time completeness notions ⋮ On helping by robust oracle machines ⋮ Masking traveling beams: optical solutions for NP-complete problems, trading space for time ⋮ The complexity of reachability in distributed communicating processes ⋮ Computing equilibria: a computational complexity perspective ⋮ On the complexity of the maximum satisfiability problem for Horn formulas ⋮ Satisfiability in many-valued sentential logic is NP-complete ⋮ Maintenance routing for train units: the interchange model ⋮ Arthur-Merlin games: A randomized proof system, and a hierarchy of complexity classes ⋮ Analyzing the complexity of finding good neighborhood functions for local search algorithms ⋮ The complexity of optimization problems ⋮ Decompositions of nondeterministic reductions ⋮ Complexity classes without machines: on complete languages for UP ⋮ LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation ⋮ Polynomially solvable satisfiability problems ⋮ Shortest enclosing walks and cycles in embedded graphs ⋮ Computational complexity of some restricted instances of 3-SAT ⋮ A hierarchy of propositional Horn formuls ⋮ Uniform data encodings ⋮ Complexity of Boolean algebras ⋮ Backtracking with multi-level dynamic search rearrangement ⋮ Spectral classes of regular, random, and empirical graphs ⋮ On the complexity of role colouring planar graphs, trees and cographs ⋮ Two-machine interval shop scheduling with time lags ⋮ Fast probabilistic algorithms for Hamiltonian circuits and matchings ⋮ Stream-based inconsistency measurement ⋮ Complexity of dimension three and some related edge-covering characteristics of graphs ⋮ The maximum infection time in the geodesic and monophonic convexities ⋮ Non existence of some mixed Moore graphs of diameter 2 using SAT ⋮ Automatic construction of optimal static sequential portfolios for AI planning and beyond ⋮ Towards a logical belief function theory ⋮ On the complexity of the constrained input selection problem for structural linear systems ⋮ The complexity of the equivalence problem for two characterizations of Presburger sets ⋮ On gamma-reducibility versus polynomial time many-one reducibility ⋮ Non deterministic polynomial optimization problems and their approximations ⋮ Optimization problems and the polynomial hierarchy ⋮ Complexity of graph embeddability problems ⋮ Probabilistic satisfiability: algorithms with the presence and absence of a phase transition ⋮ A switching algorithm for the solution of quadratic Boolean equations ⋮ Complexity of algorithms and computations ⋮ On the size of refutation Kripke models for some linear modal and tense logics ⋮ The number of depth-first searches of an ordered set ⋮ The shortest common supersequence problem over binary alphabet is NP- complete ⋮ Some simplified undecidable and NP-hard problems for simple programs ⋮ Complexity-theoretic algebra. II: Boolean algebras ⋮ On the complexity of simple arithmetic expressions ⋮ Some results on relativized deterministic and nondeterministic time hierarchies ⋮ On the structure of sets in NP and other complexity classes ⋮ A uniform approach to obtain diagonal sets in complexity classes ⋮ An effective structured approach to finding optimal partitions of networks ⋮ A note on sparse oracles for NP ⋮ On the relationship between the biconnectivity augmentation and traveling salesman problems ⋮ A state-of-the-art review of parallel-machine scheduling research ⋮ Reductions on NP and p-selective sets ⋮ On the complexity of ranking ⋮ Probabilistic bounds and algorithms for the maximum satisfiability problem ⋮ An NP-complete matching problem ⋮ Modelling and simulation of communications network planning ⋮ Sparse complete sets for NP: solution of a conjecture of Berman and Hartmanis ⋮ An improved lower bound for approximating minimum GCD multiplier in \(\ell _\infty \) norm (GCDM\(_\infty\)) ⋮ On the zero-inequivalence problem for loop programs ⋮ Scatter search and genetic algorithms for MAX-SAT problems ⋮ New complexity results about Nash equilibria ⋮ 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 ⋮ Approximability results for the maximum and minimum maximal induced matching problems ⋮ Unrestricted resolution versus N-resolution ⋮ A bounded approximation for the minimum cost 2-sat problem ⋮ On polynomial-time Turing and many-one completeness in PSPACE ⋮ The p-T-degrees of the recursive sets: Lattice embeddings, extensions of embeddings and the two-quantifier theory ⋮ George Dantzig's impact on the theory of computation ⋮ Complexity results for three-dimensional orthogonal graph drawing ⋮ A pseudo-Boolean consensus approach to nonlinear 0-1 optimization ⋮ A note on the permanent value problem ⋮ A simple proof of a theorem of Statman ⋮ On the computational complexity of integral equations ⋮ A hierarchy of tractable satisfiability problems ⋮ Decision-making coordination and efficient reasoning techniques for feature-based configuration ⋮ Alternating states for dual nondeterminism in imperative programming ⋮ The membership question for ETOL-languages is polynomially complete ⋮ The deduction theorem for strong propositional proof systems ⋮ Complexity classes for self-assembling flexible tiles ⋮ On the inapproximability of independent domination in \(2P_3\)-free perfect graphs ⋮ Hybrid commitments and their applications to zero-knowledge proof systems ⋮ Using clausal graphs to determine the computational complexity of \(k\)-bounded positive one-in-three SAT ⋮ On problems without polynomial kernels ⋮ Cryptography with constant input locality ⋮ On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls ⋮ The three-color and two-color Tantrix\(^{\text{TM}}\) rotation puzzle problems are NP-complete via parsimonious reductions ⋮ On the computation of the hull number of a graph ⋮ APX-hardness of domination problems in circle graphs ⋮ Strong nondeterministic polynomial-time reducibilities ⋮ On some natural complete operators ⋮ Complete problems in the first-order predicate calculus ⋮ Satgraphs and independent domination. I ⋮ Independent domination in hereditary classes ⋮ Current trends in substructural logics ⋮ An improved upper bound for SAT ⋮ Approximation algorithms for the maximum vertex coverage problem on bounded degree graphs ⋮ Subject-oriented spatial logic ⋮ Tractability in constraint satisfaction problems: a survey ⋮ On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Term satisfiability in \(\mathrm{FL}_{\mathrm{ew}}\)-algebras ⋮ Constrained synchronization and subset synchronization problems for weakly acyclic automata ⋮ The enduring scandal of deduction. Is propositional logic really uninformative? ⋮ A comparative runtime analysis of heuristic algorithms for satisfiability problems ⋮ Formalization and implementation of modern SAT solvers ⋮ A collaborative approach for multi-threaded SAT solving ⋮ Generating SAT instances with community structure ⋮ SAT-solving in practice, with a tutorial example from supervisory control ⋮ Augmenting measure sensitivity to detect essential, dispensable and highly incompatible features in mass customization ⋮ An approach using SAT solvers for the RCPSP with logical constraints ⋮ Computational complexity of manipulation: a survey ⋮ SAT race 2015 ⋮ Graphs with maximal induced matchings of the same size ⋮ Rainbow colouring of split graphs ⋮ Planning as satisfiability: heuristics ⋮ Algorithmic and structural aspects of the \(P_3\)-Radon number ⋮ Analysis and solving SAT and MAX-SAT problems using an \(L\)-partition approach ⋮ The complexity of computing the permanent ⋮ The paradox of inference and the non-triviality of analytic information ⋮ A complete one-way function based on a finite rank free \(\mathbb{Z}\times\mathbb{Z}\)-module ⋮ Generating meta-heuristic optimization code using ADATE ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ On the Pólya permanent problem over finite fields ⋮ Intractability and the use of heuristics in psychological explanations ⋮ Semantics and proof-theory of depth bounded Boolean logics ⋮ A note on perfect partial elimination ⋮ A decomposition method for CNF minimality proofs ⋮ A SAT-based preimage analysis of reduced \textsc{Keccak} hash functions ⋮ The pervasive reach of resource-bounded Kolmogorov complexity in computational complexity theory ⋮ Holographic algorithms: from art to science ⋮ Infeasibility of instance compression and succinct PCPs for NP ⋮ Hardness amplification within NP against deterministic algorithms ⋮ Physical portrayal of computational complexity ⋮ Towards NP-P via proof complexity and search ⋮ Boolean functions with a simple certificate for CNF complexity ⋮ An analytic criterion for CSAT ⋮ Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models ⋮ A randomized algorithm for 3-SAT ⋮ Deciding safety properties in infinite-state pi-calculus via behavioural types ⋮ Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers ⋮ Perfect state distinguishability and computational speedups with postselected closed timelike curves ⋮ Can quantum entanglement detection schemes improve search? ⋮ Most probable explanations in Bayesian networks: complexity and tractability ⋮ Topological implications of selfish neighbor selection in unstructured peer-to-peer networks ⋮ A survey on the structure of approximation classes ⋮ Guarantees and limits of preprocessing in constraint satisfaction and reasoning ⋮ Control: a perspective ⋮ Complexity of fuzzy answer set programming under Łukasiewicz semantics ⋮ Phase transitions of contingent planning problem ⋮ Efficiently embedding QUBO problems on adiabatic quantum computers ⋮ 3-SAT = SAT for a class of normal modal logics ⋮ The configurable SAT solver challenge (CSSC) ⋮ Unrelated parallel machine scheduling -- perspectives and progress ⋮ Approximating Max NAE-\(k\)-SAT by anonymous local search ⋮ On optimal approximability results for computing the strong metric dimension ⋮ Improving configuration checking for satisfiable random \(k\)-SAT instances ⋮ About some UP-based polynomial fragments of SAT ⋮ Complexity of the satisfiability problem for multilinear forms over a finite field ⋮ Variability-based model transformation: formal foundation and application ⋮ Complexity of validity for propositional dependence logics ⋮ Learning discrete decomposable graphical models via constraint optimization ⋮ On the complexity of colouring by superdigraphs of bipartite graphs ⋮ The relative complexity of analytic tableaux and SL-resolution ⋮ Finite-model theory -- A personal perspective ⋮ Feasibility problems for recurring tasks on one processor ⋮ On well-covered pentagonalizations of the plane ⋮ On the contribution of backward jumps to instruction sequence expressiveness ⋮ Collapsing and separating completeness notions under average-case and worst-case hypotheses ⋮ Non-standard approaches to integer programming ⋮ A quasi-human algorithm for solving the three-dimensional rectangular packing problem ⋮ Survey of polynomial transformations between NP-complete problems ⋮ The complexity of variable minimal formulas ⋮ Stochastic game logic ⋮ Tractable stochastic analysis in high dimensions via robust optimization ⋮ NP-completeness properties about linear extensions ⋮ Families of subsets without a given poset in double chains and Boolean lattices ⋮ Vertex 2-coloring without monochromatic cycles of fixed size is NP-complete ⋮ On the subgraph epimorphism problem ⋮ Model-based adaptive spatial sampling for occurrence map construction ⋮ A dual algorithm for the satisfiability problem ⋮ Cook reducibility is faster than Karp reducibility in NP ⋮ Algorithms for the maximum satisfiability problem ⋮ Computational experience with an interior point algorithm on the satisfiability problem ⋮ The complexity of equivalence for commutative rings ⋮ Most relevant explanation: Computational complexity and approximation methods ⋮ Fuzzy alternating automata over distributive lattices ⋮ Solving the 3-COL problem by using tissue P systems without environment and proteins on cells ⋮ On theoretical and empirical algorithmic analysis of the efficiency gap measure in partisan gerrymandering ⋮ Signsolvability revisited ⋮ A parallelization scheme based on work stealing for a class of SAT solvers ⋮ Combinatorial PCPs with short proofs ⋮ Backdoors to q-Horn ⋮ Length-bounded disjoint paths in planar graphs ⋮ Complexity of finding dense subgraphs ⋮ Nagging: A scalable fault-tolerant paradigm for distributed search ⋮ A taxonomy of complexity classes of functions ⋮ The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics ⋮ A kind of logical compilation for knowledge bases ⋮ Resolving contradictions: A plausible semantics for inconsistent systems ⋮ A linear time equivalence test for read-twice DNF formulas ⋮ Functional inversion and communication complexity ⋮ Recognition of \(q\)-Horn formulae in linear time ⋮ Problem solving by searching for models with a theorem prover ⋮ On problems with short certificates ⋮ Aggregate operations in the information source tracking method ⋮ Inversion of 2D cellular automata: Some complexity results ⋮ A bijection between cliques in graphs and factorizations in free monoids ⋮ The computational complexity of calculating partition functions of optimal medians with Hamming distance ⋮ On the complexity of labeling perspective projections of polyhedral scenes ⋮ On the complexity of some basic problems in computational convexity. I. Containment problems ⋮ Probabilistically checkable proofs and their consequences for approximation algorithms ⋮ List scheduling algorithms to minimize the makespan on identical parallel machines ⋮ Proofs of proximity for context-free languages and read-once branching programs ⋮ An average case analysis of a resolution principle algorithm in mechanical theorem proving. ⋮ Generalized resolution for 0--1 linear inequalities ⋮ Polynomial-time inference of all valid implications for Horn and related formulae ⋮ On renamable Horn and generalized Horn functions ⋮ Branch-and-cut solution of inference problems in propositional logic ⋮ On-line 2-satisfiability ⋮ Solving propositional satisfiability problems ⋮ Complexity issues in robust stability of linear delay-differential systems ⋮ A theoretical framework for cardinality-based feature models: the semantics and computational aspects ⋮ An excursion to the Kolmogorov random strings ⋮ An efficient SAT formulation for learning multiple criteria non-compensatory sorting rules from examples ⋮ A tight relationship between generic oracles and type-2 complexity theory ⋮ The number of matrices with nonzero permanent over a finite field ⋮ On the Kräuter-Seifter theorem on permanent divisibility ⋮ Infinite versions of some problems from finite complexity theory ⋮ Clifford algebra as a bridge between discrete and continuous worlds ⋮ On the complexity of entailment in propositional multivalued logics ⋮ The complexity of minimum partial truth assignments and implication in negation-free formulae ⋮ A BDD SAT solver for satisfiability testing: An industrial case study ⋮ A fast parallel SAT-solver -- efficient workload balancing ⋮ Generic hardness of the Boolean satisfiability problem ⋮ Complexity of rational and irrational Nash equilibria ⋮ Quantum one-way permutation over the finite field of two elements ⋮ NP-completeness of local colorings of graphs ⋮ On relationships between complexity classes of Turing machines ⋮ A note on implementing parallel assignment instructions ⋮ Optimal design of switched Ethernet networks implementing the multiple spanning tree protocol ⋮ Resolution and binary decision diagrams cannot simulate each other polynomially ⋮ Equivalent literal propagation in the DLL procedure ⋮ Fast algorithms for revision of some special propositional knowledge bases ⋮ Parameterized complexity of theory of mind reasoning in dynamic epistemic logic ⋮ Fully dynamic representations of interval graphs ⋮ Linearly-growing reductions of Karp's 21 NP-complete problems ⋮ Mathematical modal logic: A view of its evolution ⋮ Inverting onto functions. ⋮ 3-colorability \(\in \mathcal P\) for \(P_{6}\)-free graphs. ⋮ Unique (optimal) solutions: complexity results for identifying and locating-dominating codes ⋮ A class of facet producing graphs for vertex packing polyhedra ⋮ Boolesche Minimalpolynome und Überdeckungsprobleme ⋮ Translational lemmas, polynomial time, and \((\log n)^j\)-space ⋮ Comparing complexity classes ⋮ Constructing optimal binary decision trees is NP-complete ⋮ Some simplified NP-complete graph problems ⋮ A lower bound on the number of additions in monotone computations ⋮ Relative complexity of checking and evaluating ⋮ Complete problems for deterministic polynomial time ⋮ The polynomial-time hierarchy ⋮ Complexity-class-encoding sets ⋮ Sparse complex polynomials and polynomial reducibility ⋮ On the complexity of formal grammars ⋮ Efficient Algorithms for (3,1) Graphs ⋮ Complete sets and the polynomial-time hierarchy ⋮ Log space machines with multiple oracle tapes ⋮ On polynomial time isomorphisms of some new complete sets ⋮ On graphs with Hamiltonian squares ⋮ Cyclic ordering is NP-complete ⋮ On the complexity of regular resolution and the Davis-Putnam procedure ⋮ On log-tape isomorphisms of complete sets ⋮ The distribution of 1-widths of (0,1)-matrices ⋮ A linear-time algorithm for testing the truth of certain quantified Boolean formulas ⋮ Arithmetical hierarchy and complexity of computation ⋮ Complexity in mechanized hypothesis formation ⋮ Even initial feedback vertex set problem is NP-complete ⋮ Testing for existence of a covering Boyce-Codd normal form ⋮ On the communication complexity of zero-knowledge proofs ⋮ Strong nondeterministic Turing reduction - a technique for proving intractability ⋮ A note on the computational complexity of the pure classical implication calculus ⋮ Time-space tradeoffs for satisfiability ⋮ Computations on nondeterministic cellular automata ⋮ Sentences over integral domains and their computational complexities ⋮ A complexity analysis of bisimilarity for value-passing processes ⋮ A two-phase algorithm for solving a class of hard satisfiability problems ⋮ The relative power of logspace and polynomial time reductions ⋮ Finding the lowest free energy conformation of a protein is an NP-hard problem: Proof and implications ⋮ Randomness in interactive proofs ⋮ Towards the notion of stability of approximation for hard optimization tasks and the traveling salesman problem. ⋮ Approximating \(SVP_{\infty}\) to within almost-polynomial factors is NP-hard ⋮ Mysteries of mathematics and computation ⋮ Two results in negation-free logic ⋮ INTERVAL VERTEX-COLORINGS OF CACTUS GRAPHS WITH RESTRICTIONS ON VERTICES ⋮ Simultaneous Optimization of both Node and Edge Conservation in Network Alignment via WAVE ⋮ Completeness for nondeterministic complexity classes ⋮ Unnamed Item ⋮ A Computing Procedure for Quantification Theory ⋮ Unnamed Item ⋮ Sublinear P system solutions to NP-complete problems ⋮ Generating Difficult CNF Instances in Unexplored Constrainedness Regions ⋮ An incremental SAT-based approach for solving the real-time taxi-sharing service problem ⋮ Complexity of stability in trading networks ⋮ Machine learning and logic: a new frontier in artificial intelligence ⋮ An efficient strategy to construct a better differential on multiple-branch-based designs: application to Orthros ⋮ Reflections on Bayesian inference and Markov chain Monte Carlo ⋮ New method for combining Matsui's bounding conditions with sequential encoding method ⋮ Completing the Picture: Complexity of Graded Modal Logics with Converse ⋮ Improving complex SMT strategies with learning ⋮ Some rainbow problems in graphs have complexity equivalent to satisfiability problems ⋮ On the reliability estimation of stochastic binary systems ⋮ Getting the Lay of the Land in Discrete Space: A Survey of Metric Dimension and Its Applications ⋮ Further improvements for SAT in terms of formula length ⋮ Sequential model-based diagnosis by systematic search ⋮ Dequantizing the Quantum singular value transformation: hardness and applications to Quantum chemistry and the Quantum PCP conjecture ⋮ Intersection suffices for Boolean hierarchy equivalence ⋮ Uniformly optimally reliable graphs: A survey ⋮ Unique response Roman domination: complexity and algorithms ⋮ Complexity and heuristics for the weighted max cut‐clique problem ⋮ The 2CNF Boolean formula satisfiability problem and the linear space hypothesis ⋮ On counting propositional logic and Wagner's hierarchy ⋮ Complexity results for MCMC derived from quantitative bounds ⋮ Effective guessing has unlikely consequences ⋮ Revisiting maximum satisfiability and related problems in data streams ⋮ On computing probabilistic abductive explanations ⋮ Unnamed Item ⋮ Finding \((s,d)\)-hypernetworks in F-hypergraphs is NP-hard ⋮ IS CAUSAL REASONING HARDER THAN PROBABILISTIC REASONING? ⋮ Algorithms and complexity of strongly stable non-crossing matchings ⋮ Reducibility by means of almost polynomial functions ⋮ On the field-based division property: applications to MiMC, Feistel MiMC and GMiMC ⋮ Exact enumeration of satisfiable 2-SAT formulae ⋮ How fast can we play Tetris greedily with rectangular pieces? ⋮ SAT backdoors: depth beats size ⋮ Completeness for the complexity class \(\forall \exists \mathbb{R}\) and area-universality ⋮ Allocation of indivisible items with individual preference graphs ⋮ Parameterized Counting and Cayley Graph Expanders ⋮ Automated key recovery attacks on round-reduced Orthros ⋮ Revisiting maximum satisfiability and related problems in data streams ⋮ Refined computational complexities of hospitals/residents problem with regional caps ⋮ Complexity of the universal theory of residuated ordered groupoids ⋮ Spin Glass approach to the feedback vertex set problem ⋮ The inverse satisfiability problem ⋮ An optimization method for characterizing two groups of data ⋮ Matroid Horn functions ⋮ Indistinguishability obfuscation ⋮ Mathematics of computation through the lens of linear equations and lattices ⋮ Constrained multi-tildes ⋮ Picturing Counting Reductions with the ZH-Calculus ⋮ Words-to-Letters Valuations for Language Kleene Algebras with Variable Complements ⋮ Model Reductions for Inference: Generality of Pairwise, Binary, and Planar Factor Graphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A CNF Formula Hierarchy over the Hypercube ⋮ New problems complete for nondeterministic log space ⋮ Relativization of questions about log space computability ⋮ SPLITTING NUMBER is NP-complete ⋮ On the complexity of finite, pushdown, and stack automata ⋮ Automatic Scheduling of Periodic Event Networks by SAT Solving ⋮ Some open problems in the theory of computation as questions about two-way deterministic pushdown automaton languages ⋮ Graph colourings and partitions ⋮ Power indices and easier hard problems ⋮ Complexity-theoretic aspects of expanding cellular automata ⋮ Time-space tradeoffs for SAT on nonuniform machines ⋮ Advice complexity of priority algorithms ⋮ Approximate evaluations of characteristic polynomials of Boolean functions ⋮ Statistical mechanics methods and phase transitions in optimization problems ⋮ Rigorous results for random (\(2+p)\)-SAT ⋮ Results related to threshold phenomena research in satisfiability: Lower bounds ⋮ Lower bounds for random 3-SAT via differential equations ⋮ Hardness and methods to solve CLIQUE ⋮ Approximating the minimum hub cover problem on planar graphs ⋮ On the complexity of dataflow analysis of logic programs ⋮ Approximate set union via approximate randomization ⋮ Approximate set union via approximate randomization ⋮ The Deduction Theorem for Strong Propositional Proof Systems ⋮ Satisfiability of Algebraic Circuits over Sets of Natural Numbers ⋮ Determining Whether a Simplicial 3-Complex Collapses to a 1-Complex Is NP-Complete ⋮ Parameterised complexity of model checking and satisfiability in propositional dependence logic ⋮ On the decidability of finding a positive ILP-instance in a regular set of ILP-instances ⋮ Lower bounds for the happy coloring problems ⋮ Graphs with large total angular resolution ⋮ Unnamed Item ⋮ Generating all vertices of a polyhedron is hard ⋮ Implementing NChooseK on IBM Q Quantum Computer Systems ⋮ Logic and Complexity in Cognitive Science ⋮ Unnamed Item ⋮ A Short Essay towards if P not equal NP ⋮ Approximating Minimum Representations of Key Horn Functions ⋮ Study of discrete automaton models of gene networks of nonregular structure using symbolic calculations ⋮ Almost all Classical Theorems are Intuitionistic ⋮ A note on complete sets and transitive closure ⋮ Vertices Belonging to All or to No Maximum Stable Sets of a Graph ⋮ The Bayesian ontology language \(\mathcal {BEL}\) ⋮ A complexity theory for feasible closure properties ⋮ Computational complexity of inner and outer \(j\)-radii of polytopes in finite-dimensional normed spaces ⋮ Ground State Connectivity of Local Hamiltonians ⋮ Proofs of Proximity for Context-Free Languages and Read-Once Branching Programs ⋮ The polynomial hierarchy and a simple model for competitive analysis ⋮ Symbioses between mathematical logic and computer science ⋮ A unified framework for DPLL(T) + certificates ⋮ Local Search to Approximate Max NAE-$$k$$-Sat Tightly ⋮ Propositional SAT Solving ⋮ Local and global deadlock-detection in component-based systems are NP-hard ⋮ Is the protein model assignment problem under linked branch lengths NP-hard? ⋮ Counting for satisfiability by inverting resolution ⋮ Progress in quantum algorithms ⋮ Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems ⋮ Hardness assumptions in the foundations of theoretical computer science ⋮ Exploiting partial knowledge of satisfying assignments ⋮ On the Complexity of the Minimum Independent Set Partition Problem ⋮ Unnamed Item ⋮ A novel characterization of the complexity class \(\Theta_k^{\mathrm{P}}\) based on counting and comparison ⋮ Zero knowledge and circuit minimization ⋮ Some modifications of auxiliary pushdown automata ⋮ Complexity of Propositional Independence and Inclusion Logic ⋮ QMA with Subset State Witnesses ⋮ Machines that perform measurements ⋮ Signatures and Efficient Proofs on Committed Graphs and NP-Statements ⋮ Generating hard satisfiability problems ⋮ Computational complexity of the word problem in modal and Heyting algebras with a small number of generators ⋮ Complexity and Algorithms for Well-Structured k-SAT Instances ⋮ Generalized probabilistic satisfiability and applications to modelling attackers with side-channel capabilities ⋮ Decidability of NP-complete problems ⋮ Levenshtein graphs: resolvability, automorphisms \& determining sets ⋮ A Boolean satisfiability approach to the resource-constrained project scheduling problem ⋮ A multistage view on 2-satisfiability ⋮ Barnette's conjecture through the lens of the \(Mod_k P\) complexity classes ⋮ Factor models on locally tree-like graphs ⋮ OnP-subset structures ⋮ Boolean functions with long prime implicants ⋮ The complexity of computing the behaviour of lattice automata on infinite trees ⋮ The Three-Color and Two-Color TantrixTM Rotation Puzzle Problems Are NP-Complete Via Parsimonious Reductions ⋮ Boundary properties of the satisfiability problems ⋮ A linear kernel for the complementary maximal strip recovery problem ⋮ The Power of Self-Reducibility: Selectivity, Information, and Approximation ⋮ MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability ⋮ Physical consequences of P≠NP and the density matrix renormalization group annealing conjecture ⋮ Organization mechanism and counting algorithm on vertex-cover solutions ⋮ The large deviations of the whitening process in random constraint satisfaction problems ⋮ Decomposing SAT Instances with Pseudo Backbones ⋮ Characterization and recognition of generalized clique-Helly graphs ⋮ On variable-weighted exact satisfiability problems ⋮ Visualizing SAT instances and runs of the DPLL algorithm ⋮ DPLL: The Core of Modern Satisfiability Solvers ⋮ Conflict analysis in mixed integer programming ⋮ Unnamed Item ⋮ On problems for which no oracle can help ⋮ Extended resolution simulates binary decision diagrams ⋮ Partial bi-immunity, scaled dimension, and NP-completeness ⋮ Pairs of SAT-assignments in random Boolean formulæ ⋮ Using the renormalization group to classify Boolean functions ⋮ Reductions, completeness and the hardness of approximability ⋮ Edmonds polytopes and a hierarchy of combinatorial problems. (Reprint) ⋮ On propositional coding techniques for the distinguishability of objects in finite sets ⋮ Incremental delay enumeration: space and time ⋮ Zeon and idem-Clifford formulations of Boolean satisfiability ⋮ Satisfiability problems for propositional calculi ⋮ The complexity of dissociation set problems in graphs ⋮ New tractable classes for default reasoning from conditional knowledge bases ⋮ Complexity-theoretic aspects of expanding cellular automata ⋮ Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games ⋮ Clause vivification by unit propagation in CDCL SAT solvers ⋮ How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning ⋮ Finding a Forest in a Tree ⋮ Moment subset sums over finite fields ⋮ Definability for model counting ⋮ Comparative Analysis of Random Generators ⋮ Editorial: Symbolic computation and satisfiability checking ⋮ Minimizing Sum of Truncated Convex Functions and Its Applications ⋮ Low-dimensional representation of genomic sequences ⋮ The Boolean satisfiability problem in Clifford algebra ⋮ Learning action models with minimal observability ⋮ Edmonds polytopes and a hierarchy of combinatorial problems ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Formally verifying the solution to the Boolean Pythagorean triples problem ⋮ Relative complexity of algebras ⋮ A note on context free languages, complexity classes, and diagonalization ⋮ Improved WPM encoding for coalition structure generation under MC-nets ⋮ Balance problems for integer circuits ⋮ The 2004 Benjamin Franklin medal in computer and cognitive science presented to Richard M. Karp ⋮ Descriptive complexity and revealed preference theory ⋮ Families of nested graphs with compatible symmetric-group actions ⋮ On Dinur’s proof of the PCP theorem ⋮ A new exact algorithm for the multi-depot vehicle routing problem under capacity and route length constraints ⋮ Characterising the complexity of constraint satisfaction problems defined by 2-constraint forbidden patterns ⋮ Speeding up operations on feature terms using constraint programming and variable symmetry ⋮ Complexity classes and theories of finite models ⋮ Complexity of node coverage games ⋮ No easy puzzles: hardness results for jigsaw puzzles ⋮ Mining circuit lower bound proofs for meta-algorithms ⋮ Roof duality, complementation and persistency in quadratic 0–1 optimization ⋮ Property testers for dense constraint satisfaction programs on finite domains ⋮ Analysis of periodic linear systems over finite fields with and without Floquet transform ⋮ Improving a fixed parameter tractability time bound for the shadow problem ⋮ Adaptive memory search for Boolean optimization problems ⋮ Reasoning with ordered binary decision diagrams ⋮ Precise interprocedural dependence analysis of parallel programs ⋮ Approximation algorithms for the optimal \(p\)-source communication spanning tree ⋮ Polynomial transformations and data-independent neighborhood functions ⋮ Towards a unified approach to black-box constructions of zero-knowledge proofs ⋮ Peripherality in networks: theory and applications ⋮ Positive planar satisfiability problems under 3-connectivity constraints ⋮ Automatic search for bit-based division property ⋮ On the \(k\)-colored rainbow sets in fixed dimensions ⋮ Computational properties of partial non-deterministic matrices and their logics ⋮ Computers and universal algebra: Some directions ⋮ From the \(W\)-hierarchy to XNLP. Classes of fixed parameter intractability ⋮ A modal view on resource-bounded propositional logics ⋮ Perfect Italian domination in graphs: complexity and algorithms ⋮ A primal-dual approximation algorithm for \textsc{minsat} ⋮ Is my attack tree correct? ⋮ PALO: a probabilistic hill-climbing algorithm ⋮ Propositional truth maintenance systems: Classification and complexity analysis ⋮ The generalized definitions of the two-dimensional largest common substructure problems ⋮ Placing quantified variants of 3-SAT and \textsc{not-all-equal} 3-SAT in the polynomial hierarchy ⋮ The analysis of expected fitness and success ratio of two heuristic optimizations on two bimodal MaxSat problems ⋮ The place of logic in reasoning ⋮ Lewis dichotomies in many-valued logics ⋮ The complete set of minimal simple graphs that support unsatisfiable 2-CNFs ⋮ Optimal scaling of random-walk Metropolis algorithms on general target distributions ⋮ Threshold behaviors of a random constraint satisfaction problem with exact phase transitions ⋮ Complexity results for modal dependence logic ⋮ Percolation on fitness landscapes: effects of correlation, phenotype, and incompatibilities ⋮ The complexity of problems for quantified constraints ⋮ Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results ⋮ Recognition of tractable satisfiability problems through balanced polynomial representations ⋮ Generating clause sequences of a CNF formula ⋮ On \(k\)-positive satisfiability problem ⋮ Facets from gadgets ⋮ Orthogonal drawings of graphs for the automation of VLSI circuit design ⋮ On simplified NP-complete variants of \textsc{Monotone} 3\textsc{-Sat} ⋮ Constrained pseudo-propositional logic ⋮ \(\boldsymbol{borealis}\) -- a generalized global update algorithm for Boolean optimization problems ⋮ Independent transversals of hypergraph edges and bipartite bigraphs ⋮ Faradžev Read-type enumeration of non-isomorphic CC systems ⋮ Simultaneous visibility representations of undirected pairs of graphs ⋮ Improved algorithms for the general exact satisfiability problem ⋮ Cook's versus Valiant's hypothesis ⋮ Strongly stable and maximum weakly stable noncrossing matchings ⋮ Open-world probabilistic databases: semantics, algorithms, complexity ⋮ Propositional proof systems based on maximum satisfiability ⋮ VF2++ -- an improved subgraph isomorphism algorithm ⋮ Generalized probabilistic satisfiability ⋮ Type-two polynomial-time and restricted lookahead ⋮ Ising formulations of some graph-theoretic problems in psychological research: models and methods ⋮ On distance-preserving elimination orderings in graphs: complexity and algorithms ⋮ Lee-Yang theorems and the complexity of computing averages ⋮ The fair OWA one-to-one assignment problem: NP-hardness and polynomial time special cases ⋮ Angelic processes for CSP via the UTP ⋮ Hardness results for approximate pure Horn CNF formulae minimization ⋮ Resource-constrained project scheduling with activity splitting and setup times ⋮ Steady states in the scheduling of discrete-time systems ⋮ TANTRIX\(^{\text{TM}}\) rotation puzzles are intractable ⋮ \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT ⋮ A new tractable class of constraint satisfaction problems ⋮ Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances ⋮ Isomorphic implication ⋮ A formal methods approach to predicting new features of the eukaryotic vesicle traffic system ⋮ Improved haplotype assembly using Xor genotypes ⋮ On irreduceability of Boolean functions with respect to commutative associative operation ⋮ Solving a real constraint satisfaction model for the university course timetabling problem: a case study ⋮ The complexity of error metrics ⋮ Selecting and covering colored points ⋮ A unifying model for locally constrained spanning tree problems ⋮ Directed hypergraphs and applications ⋮ Combinatorial optimization algorithms for detecting collapse mechanisms of concrete slabs ⋮ Algorithmic reduction of biological networks with multiple time scales ⋮ On the complexity of asynchronous freezing cellular automata ⋮ The opacity of backbones ⋮ An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses ⋮ Sorting, linear time and the satisfiability problem ⋮ Asymptotic density and computability ⋮ Enumerative counting is hard ⋮ On some FPT problems without polynomial Turing compressions ⋮ Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search ⋮ Asymptotic connectedness of random interval graphs in a one dimensional data delivery problem ⋮ On the NP-hardness of edge-deletion and -contraction problems ⋮ Context-sensitive fusion grammars and fusion grammars with forbidden context are universal ⋮ Solving satisfiability problems using elliptic approximations -- effective branching rules ⋮ Worst-case analysis of clique MIPs ⋮ Black-box use of one-way functions is useless for optimal fair coin-tossing ⋮ On an optimal propositional proof system and the structure of easy subsets of TAUT. ⋮ On the Hamming distance of constraint satisfaction problems. ⋮ Unification algorithms cannot be combined in polynomial time. ⋮ The complexity of propositional linear temporal logics in simple cases ⋮ Symbolic model checking of timed guarded commands using difference decision diagrams ⋮ Ranking with multiple reference points: efficient SAT-based learning procedures ⋮ Assessing progress in SAT solvers through the Lens of incremental SAT ⋮ On the hierarchical community structure of practical Boolean formulas ⋮ A fast algorithm for SAT in terms of formula length ⋮ Parameterized complexity of \((A,\ell)\)-path packing ⋮ A model of random industrial SAT ⋮ Improved Integral Attack on Generalized Feistel Cipher ⋮ Logical derivation search with assumption traceability ⋮ On Tackling Explanation Redundancy in Decision Trees ⋮ Strongly Stable and Maximum Weakly Stable Noncrossing Matchings ⋮ Unnamed Item ⋮ Resource-bounded kolmogorov complexity revisited ⋮ Recent results in hardness of approximation ⋮ Disordered systems insights on computational hardness ⋮ On an optimal quantified propositional proof system nal proof system and a complete language for NP ∩ co-NP for NP ∩ co-NP ⋮ An urban transportation problem solved by parallel programming with hyper-heuristics ⋮ Autour de nouvelles notions pour l'analyse des algorithmes d'approximation : formalisme unifié et classes d'approximation ⋮ Smoothing the Gap Between NP and ER ⋮ Counting Small Induced Subgraphs Satisfying Monotone Properties ⋮ Satisfiability in Boolean Logic (SAT problem) is polynomial? ⋮ Deciding Parity Games in Quasi-polynomial Time ⋮ On Double-Resolution Imaging and Discrete Tomography ⋮ Generalized theorems on relationships among reducibility notions to certain complexity classes ⋮ Unnamed Item ⋮ Optimization under Decision-Dependent Uncertainty ⋮ NP-completeness: A retrospective ⋮ On black-box optimization in divide-and-conquer SAT solving ⋮ THE RECOGNITION COMPLEXITY OF DECIDABLE THEORIES ⋮ Causal Rule Sets for Identifying Subgroups with Enhanced Treatment Effects ⋮ Winning a Pool Is Harder Than You Thought ⋮ Testing membership: Beyond permutation groups ⋮ On monotonous oracle machines ⋮ A decade of TAPSOFT ⋮ The theory of the polynomial many-one degrees of recursive sets is undecidable ⋮ INTERVAL EDGE-COLORINGS OF TREES WITH RESTRICTIONS ON THE EDGES ⋮ Counting single-qubit Clifford equivalent graph states is #P-complete ⋮ Unnamed Item ⋮ Algebraic Attacks against Random Local Functions and Their Countermeasures ⋮ Bisimulations of Boolean Control Networks ⋮ Unnamed Item ⋮ Phase transitions in theq-coloring of random hypergraphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Resolvability of Hamming Graphs ⋮ Constraint and Satisfiability Reasoning for Graph Coloring ⋮ A quantum differentiation ofk-SAT instances ⋮ Dynamical Systems Theory and Algorithms for NP-hard Problems ⋮ The Time Complexity of Permutation Routing via Matching, Token Swapping and a Variant ⋮ Extending time‐to‐target plots to multiple instances ⋮ Unnamed Item ⋮ Breaking Cycle Structure to Improve Lower Bound for Max-SAT ⋮ Computing quantum discord is NP-complete ⋮ ANALYSIS AND SOLUTION OF DISCRETE OPTIMIZATION PROBLEMS WITH LOGICAL CONSTRAINTS ON THE BASE OF L-PARTITION APPROACH ⋮ ON GENERIC COMPLEXITY OF THE VALIDITY PROBLEM FOR BOOLEAN FORMULAS ⋮ ON GENERIC NP-COMPLETENESS OF THE BOOLEAN SATISFIABILITY PROBLEM ⋮ ON COMPLEXITY OF THE SATISFIABILITY PROBLEM OF SYSTEMS OVER FINITE POSETS ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ DECIDABILITY OF THE RESTRICTED THEORIES OF A CLASS OF PARTIAL ORDERS ⋮ Finding Effective SAT Partitionings Via Black-Box Optimization ⋮ A simple tableau system for the logic of elsewhere ⋮ Unification algorithms cannot be combined in polynomial time ⋮ Inductive Complexity of P versus NP Problem ⋮ Finding Optimal Implementations of Non-native CNOT Gates Using SAT ⋮ On generating all solutions of generalized satisfiability problems ⋮ The complexity of scheduling TV commercials ⋮ Linear-Time Algorithm for Quantum 2SAT ⋮ Branching Process Approach for 2-Sat Thresholds ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Hybrid ASP-based Approach to Pattern Mining ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Using Merging Variables-Based Local Search to Solve Special Variants of MaxSAT Problem ⋮ Canonical Models and the Complexity of Modal Team Logic ⋮ NP-Complete operations research problems and approximation algorithms ⋮ P-selective sets, tally languages, and the behavior of polynomial time reducibilities onNP ⋮ On the Complexity of Local Graph Transformations ⋮ Low order polynomial bounds on the expected performance of local improvement algorithms ⋮ Graph isomorphism is low for PP ⋮ Real-time computations with restricted nondeterminism ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Boolean satisfiability in quantum compilation ⋮ Model Checking and Validity in Propositional and Modal Inclusion Logics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Scalable Algorithms for Multiple Network Alignment ⋮ On the Complexity of Inverse Mixed Integer Linear Optimization ⋮ Backdoors into Two Occurrences ⋮ A Unified Framework for Multistage Mixed Integer Linear Optimization ⋮ LaserTank is NP-Complete ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Towards the Actual Relationship Between NP and Exponential Time ⋮ Trivial integer programs unsolvable by branch-and-bound ⋮ Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals
This page was built for publication: The complexity of theorem-proving procedures
