A linear-time algorithm for testing the truth of certain quantified Boolean formulas
From MaRDI portal
Publication:1254112
DOI10.1016/0020-0190(79)90002-4zbMath0398.68042OpenAlexW2031823362WikidataQ29394502 ScholiaQ29394502MaRDI QIDQ1254112
Michael F. Plass, Bengt Aspvall, Robert Endre Tarjan
Publication date: 1979
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0020-0190(79)90002-4
Components of a Directed GraphFinding Strongly ConnectedLinear-Time AlgorithmTesting the Truth of Quantified Boolean Formulas
Related Items
Local base station assignment with time intervals in mobile computing environments, Probabilistic state estimation for labeled continuous time Markov models with applications to attack detection, An efficiently solvable graph partition problem to which many problems are reducible, 2-satisfiability and diagnosing fault processors in massively parallel computing systems, A new algorithm for the propositional satisfiability problem, Satisfiability with index dependency, An algorithm for random signed 3-SAT with intervals, Is the protein model assignment problem under linked branch lengths NP-hard?, Decomposability of partially defined Boolean functions, Planar straight-line realizations of 2-trees with prescribed edge lengths, Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems, Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing, Boolean functions as models for quantified Boolean formulas, Domain permutation reduction for constraint satisfaction problems, What makes propositional abduction tractable, Unnamed Item, Unnamed Item, A recognition algorithm for adjusted interval digraphs, The network-untangling problem: from interactions to activity timelines, 4-coloring \((P_6, \text{bull})\)-free graphs, Makespan minimization on unrelated parallel machines with a few bags, The price of defense, Recognizing simple-triangle graphs by restricted 2-chain subgraph cover, On the complexity of cd-coloring of graphs, The satisfiability constraint gap, Some pitfalls for experimenters with random SAT, A recognition algorithm for simple-triangle graphs, Automatic refinement to efficient data structures: a comparison of two approaches, 3-colouring AT-free graphs in polynomial time, The complexity of binary matrix completion under diameter constraints, Regular switching components, Matching cut: kernelization, single-exponential time FPT, and exact exponential algorithms, The complete set of minimal simple graphs that support unsatisfiable 2-CNFs, Jointly stable matchings, Integer feasibility and refutations in UTVPI constraints using bit-scaling, The \(r\)-coloring and maximum stable set problem in hypergraphs with bounded matching number and edge size, A tighter upper bound for random MAX \(2\)-SAT, A framework for certified Boolean branch-and-bound optimization, A multistage view on 2-satisfiability, Two polynomial time graph labeling algorithms optimizing max-norm-based objective functions, Extended skew partition problem, On the exact complexity of evaluating quantified \(k\)-\textsc{cnf}, Complexity and algorithms for recognizing polar and monopolar graphs, Maximum renamable Horn sub-CNFs, Satisfiability threshold for random XOR-CNF formulas, The \(Multi\)-SAT algorithm, A remark on random 2-SAT, Two tractable subclasses of minimal unsatisfiable formulas, Recognition of tractable satisfiability problems through balanced polynomial representations, Semidefinite resolution and exactness of semidefinite relaxations for satisfiability, On \(k\)-positive satisfiability problem, Facets from gadgets, Boundary properties of the satisfiability problems, Exploiting independent subformulas: a faster approximation scheme for \(\# k\)-SAT, Bounded-width QBF is PSPACE-complete, The scaling window of the 2-SAT transition, Labeling nonograms: boundary labeling for curve arrangements, On variable-weighted exact satisfiability problems, On a decision procedure for quantified linear programs, Visualizing SAT instances and runs of the DPLL algorithm, Polar SAT and related graphs, Optimization for first order Delaunay triangulations, A polynomial-time algorithm to find an equitable home--away assignment, A note on the recognition of bisplit graphs, Unconstrained 0-1 optimization and Lagrangean relaxation, Three-coloring and list three-coloring of graphs without induced paths on seven vertices, The cd-Coloring of Graphs, Consistent query answering for primary keys in Datalog, As Close as It Gets, Selecting and covering colored points, Constraint-generating dependencies, New and improved algorithms for unordered tree inclusion, Faster graph bipartization, An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses, Stable matching with uncertain linear preferences, Solving and sampling with many solutions, Compact linear programs for 2SAT, Detecting strong cliques, On the r,s-SAT satisfiability problem and a conjecture of Tovey, New complexity results for Łukasiewicz logic, NodeTrix planarity testing with small clusters, Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas, Minimal distance of propositional models, Bisplit graphs, On subclasses of minimal unsatisfiable formulas, Bounds and fast approximation algorithms for binary quadratic optimzation problems with application to MAX 2SAT, Worst-case analysis of clique MIPs, An introduction to periodical discrete sets from a tomographical perspective, Recognition and dualization of disguised bidual Horn functions., The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas, A short note on some tractable cases of the satisfiability problem., Reconstruction of convex polyominoes from orthogonal projections of their contours, SAT distributions with planted assignments and phase transitions between decision and optimization problems, The complexity of string partitioning, Parameterized complexity of stable roommates with ties and incomplete lists through the lens of graph parameters, Detection of the discrete convexity of polyominoes, A perspective on certain polynomial-time solvable classes of satisfiability, Disconnectivity and relative positions in simultaneous embeddings, The number of 2-SAT functions, Space efficient merging of de Bruijn graphs and Wheeler graphs, Reconstruction of convex polyominoes with a blocking component, Disjunctions, independence, refinements, Incorporating bounds from decision diagrams into integer programming, Datalog rewritability of disjunctive Datalog programs and non-Horn ontologies, Recognition of \(q\)-Horn formulae in linear time, Recognizing and drawing IC-planar graphs, Complexity versus stability for classes of propositional formulas, Minimization of a quadratic pseudo-Boolean function, The complexity of constraint satisfaction games and QCSP, Superpolynomial lower bounds for the \((1+1)\) EA on some easy combinatorial problems, Red-blue clique partitions and \((1-1)\)-transversals, Index minimization of differential-algebraic equations in hybrid analysis for circuit simulation, The unique Horn-satisfiability problem and quadratic Boolean equations., Polynomial-time inference of all valid implications for Horn and related formulae, On renamable Horn and generalized Horn functions, On-line 2-satisfiability, Positive and Horn decomposability of partially defined Boolean functions, An extension of the König-Egerváry property to node-weighted bidirected graphs, Density condensation of Boolean formulas, Optimizing propositional calculus formulas with regard to questions of deducibility, Classical, quantum and nonsignalling resources in bipartite games, On testing monomials in multivariate polynomials, Algorithms solving the matching cut problem, An algorithm reconstructing convex lattice sets., New results on edge partitions of 1-plane graphs, Non-Horn clause logic programming, The maximum length of prime implicates for instances of 3-SAT, Semantics and complexity of abduction from default theories, A randomized algorithm for 3-SAT, Reasoning about visibility, A fast algorithm for solving systems of linear equations with two variables per equation, The minimum spanning tree problem with conflict constraints and its variations, Seriation in the presence of errors: a factor 16 approximation algorithm for \(l_{\infty }\)-fitting Robinson structures to distances, On the structure and the number of prime implicants of 2-\(\mathsf{CNF}\)s, A switching algorithm for the solution of quadratic Boolean equations, Solving MAX-\(r\)-SAT above a tight lower bound, Testing the simultaneous embeddability of two graphs whose intersection is a biconnected or a connected graph, Existence of simple propositional formulas, Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search, Probabilistic bounds and algorithms for the maximum satisfiability problem, Locally constrained graph homomorphisms -- structure, complexity, and applications, Colouring, constraint satisfaction, and complexity, A logic-based approach to polymer sequence analysis, Solving peptide sequencing as satisfiability, The predecessor-existence problem for \(k\)-reversible processes, An algorithmic toolbox for periodic partial words, Path-driven orientation of mixed graphs, Bounded list injective homomorphism for comparative analysis of protein-protein interaction graphs, Computing \(H\)-joins with application to 2-modular decomposition, An analytical approach to global optimization, Recognition of unipolar and generalised split graphs, Co-clustering under the maximum norm, Parameterized complexity analysis for the closest string with wildcards problem, Reconstructing convex polyominoes from horizontal and vertical projections, A complexity dichotomy for matching cut in (bipartite) graphs of fixed diameter, Models and quantifier elimination for quantified Horn formulas, Quell, An algorithm for finding homogeneous pairs, Algorithms for media, Capturing complexity classes by fragments of second-order logic, A Max-flow approach to improved lower bounds for quadratic unconstrained binary optimization (QUBO), An algorithmic framework for labeling network maps, Complexity results for three-dimensional orthogonal graph drawing, Simultaneous embedding: edge orderings, relative positions, cutvertices, A pseudo-Boolean consensus approach to nonlinear 0-1 optimization, An efficient algorithm for the 3-satisfiability problem, Rule set design problems for oritatami systems, The P versus NP-complete dichotomy of some challenging problems in graph theory, Efficient branch-and-bound algorithms for weighted MAX-2-SAT, The Helly property and satisfiability of Boolean formulas defined on set families, Quantified constraint satisfaction and the polynomially generated powers property, Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances, Generalized \(k\)-ary tanglegrams on level graphs: a satisfiability-based approach and its evaluation, On exact selection of minimally unsatisfiable subformulae, Solving the resolution-free SAT problem by submodel propagation in linear time, Toward leaner binary-clause reasoning in a satisfiability solver, Upper and lower bounds for finding connected motifs in vertex-colored graphs, Rainbow graph splitting, Minimum sum of diameters clustering, Satisfiability of mixed Horn formulas, Algorithms for unipolar and generalized split graphs, Efficient algorithms for network localization using cores of underlying graphs, The complexity of satisfiability problems: Refining Schaefer's theorem, Red-blue covering problems and the consecutive ones property, Algorithms for the maximum satisfiability problem, Optimal cell flipping to minimize channel density in VLSI design and pseudo-Boolean optimization, Probe threshold and probe trivially perfect graphs, On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls, Backdoor sets of quantified Boolean formulas, Simulated annealing for the unconstrained quadratic pseudo-Boolean function, The complexity of the satisfiability problem for Krom formulas, Reconstruction of convex 2D discrete sets in polynomial time, Logical analysis of binary data with missing bits, On functional dependencies in \(q\)-Horn theories, Uniquely solvable quadratic Boolean equations, Reconstructing \(hv\)-convex polyominoes from orthogonal projections, Random 2-SAT and unsatisfiability, Improving exact algorithms for MAX-2-SAT, Backdoors to q-Horn, Seriation in the presence of errors: NP-hardness of \(l_{\infty}\)-fitting Robinson structures to dissimilarity matrices, Autarkies and Persistencies for QUBO, Boolean analysis of incomplete examples, Tiling with bars and satisfaction of boolean formulas, Backdoors to Satisfaction, Quasi-Linear-Time Algorithms by Generalisation of Union-Find in CHR, A linear expected-time algorithm for deriving all logical conclusions implied by a set of boolean inequalities, Random k -SAT and the power of two choices, Smooth and sharp thresholds for random{k}-XOR-CNF satisfiability, Smooth and sharp thresholds for random{k}-XOR-CNF satisfiability, Unnamed Item, Co-Clustering Under the Maximum Norm, Algorithms Solving the Matching Cut Problem, Complexity of \(C_k\)-coloring in hereditary classes of graphs, Reconstruction of Convex Sets from One or Two X-rays, On the impact of stratification on the complexity of nonmonotonic reasoning, The number of satisfying assignments of random 2‐SAT formulas, New Results on the Phase Transition for Random Quantified Boolean Formulas, Computation of Renameable Horn Backdoors, A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors, A CNF Class Generalizing Exact Linear Formulas, A first polynomial non-clausal class in many-valued logic, Reachability in choice networks, Fairness in temporal slot assignment, Partial and simultaneous transitive orientations via modular decompositions, Exact enumeration of satisfiable 2-SAT formulae, SAT backdoors: depth beats size, Efficiently recognizing graphs with equal independence and annihilation numbers, Computing NodeTrix Representations of Clustered Graphs, Algorithms and complexity of sandwich problems in graphs (extended abstract), The parameterized complexity of guarding almost convex polygons, Unnamed Item, Quantified Constraint Satisfaction and the Polynomially Generated Powers Property, Unnamed Item, OnP-subset structures, 4‐Coloring P 6 ‐Free Graphs with No Induced 5‐Cycles, A quantum differentiation ofk-SAT instances, Ground states of unfrustrated spin Hamiltonians satisfy an area law, A CNF Formula Hierarchy over the Hypercube, Quantified Constraints in Twenty Seventeen, No-Wait Scheduling for Locks, Absorbing random walks and the NAE2SAT problem, Bounds on the size of PC and URC formulas, Decomposing SAT Instances with Pseudo Backbones, Satisfiability threshold for power law random 2-SAT in configuration model, A Satisfiability-Based Approach for Embedding Generalized Tanglegrams on Level Graphs, RECONSTRUCTION OF TWO SUBCLASSES OF 2L-CONVEX POLYOMINOES, On the use of graphs in discrete tomography, On the use of graphs in discrete tomography, Between 2- and 3-colorability, On generating all solutions of generalized satisfiability problems, Linear-Time Algorithm for Quantum 2SAT, Tractability of quantified temporal constraints to the max, Branching Process Approach for 2-Sat Thresholds, Disjoint clique cutsets in graphs without long holes, Unnamed Item, Unnamed Item, A lower bound on CNF encodings of the at-most-one constraint, Comparison of algorithms for reconstructing \(hv\)-convex discrete sets, Reconstruction of 4- and 8-connected convex discrete sets from row and column projections, Recognition and drawing of stick graphs, On the Exact Complexity of Evaluating Quantified k-CNF, Unnamed Item, The Uniform Minimum-Ones 2SAT Problem and its Application to Haplotype Classification, Random 2-SAT: Results and problems, Bipartite graphs of small readability, On Structural Parameterizations of Hitting Set: Hitting Paths in Graphs Using 2-SAT, On Structural Parameterizations of Hitting Set: Hitting Paths in Graphs Using 2-SAT, Graph isomorphism restricted by lists, Cвойства систем образующих универсальных алгебр, порождаемых булевыми биюнктивными функциями, Unnamed Item, Unnamed Item, CASCADING RANDOM WALKS, A threshold for unsatisfiability, On Restricted Disjunctive Temporal Problems: Faster Algorithms and Tractability Frontier, NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability, A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints, On Some Aspects of Mixed Horn Formulas, On memoryless provers and insincere verifiers, k-SAT Is No Harder Than Decision-Unique-k-SAT, Adding clauses to poor man's logic (without increasing the complexity), Unnamed Item, Unnamed Item, Convex Aggregation Problems in $$\mathbb {Z}^2$$, Unnamed Item, Exact location of the phase transition for random (1,2)-QSAT, Variations on Instant Insanity, Delaying satisfiability for random 2SAT, Entropy of theK-Satisfiability Problem, Solution-Graphs of Boolean Formulas and Isomorphism1, SAT Distributions with Phase Transitions between Decision and Optimization Problems, On the restricted equivalence for subclasses of propositional logic, Roof duality, complementation and persistency in quadratic 0–1 optimization
Cites Work
