New methods for 3-SAT decision and worst-case analysis

DOI10.1016/S0304-3975(98)00017-6zbMath0930.68066OpenAlexW2066749637MaRDI QIDQ1960406

Oliver Kullmann

Publication date: 12 January 2000

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(98)00017-6

zbMATH Keywords

analysis of algorithmsblocked clauses3-SATextended resolutionworst-case upper boundsgeneralized autarkness

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items (41)

Parameterized enumeration, transversals, and imperfect phylogeny reconstruction ⋮ Counting Maximal Independent Sets in Subcubic Graphs ⋮ Computing the similarity of two sequences with nested arc annotations ⋮ Efficient 3-SAT algorithms in the tile assembly model ⋮ New upper bound for the \#3-SAT problem ⋮ A top-down approach to search-trees: Improved algorithmics for 3-hitting set ⋮ Exploiting partial knowledge of satisfying assignments ⋮ The complexity of pure literal elimination ⋮ Simulating circuit-level simplifications on CNF ⋮ Algorithms for four variants of the exact satisfiability problem ⋮ Unnamed Item ⋮ New upper bounds for the problem of maximal satisfiability ⋮ A universally fastest algorithm for Max 2-sat, Max 2-CSP, and everything in between ⋮ A randomized algorithm for 3-SAT ⋮ Sharp separation and applications to exact and parameterized algorithms ⋮ Improving \(3N\) circuit complexity lower bounds ⋮ Exact algorithms for edge domination ⋮ Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT. ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ On the complexity of unique circuit SAT ⋮ Branch and recharge: exact algorithms for generalized domination ⋮ New methods for 3-SAT decision and worst-case analysis ⋮ On a generalization of extended resolution ⋮ Complexity analysis of propositional resolution with autarky pruning ⋮ On the number of minimal transversals in 3-uniform hypergraphs ⋮ Quantifier elimination by dependency sequents ⋮ Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT ⋮ Improved algorithms for the general exact satisfiability problem ⋮ On the number of 2-packings in a connected graph ⋮ Counting models for 2SAT and 3SAT formulae ⋮ Solving the resolution-free SAT problem by submodel propagation in linear time ⋮ Improving Efficiency of 3-SAT-Solving Tile Systems ⋮ Solving NP-Complete Problems with Quantum Search ⋮ CASCADING RANDOM WALKS ⋮ The Lovász Local Lemma and Satisfiability ⋮ Counting Independent Sets in Claw-Free Graphs ⋮ On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls ⋮ Unnamed Item ⋮ Investigations on autark assignments ⋮ Present and Future of Practical SAT Solving ⋮ A deterministic \((2-2/(k+1))^{n}\) algorithm for \(k\)-SAT based on local search.

Uses Software

• DIMACS

Cites Work

• Number of models and satisfiability of sets of clauses
• Solving satisfiability in less than \(2^ n\) steps
• A satisfiability tester for non-clausal propositional calculus
• Two systems for proving tautologies, based on the split method
• Branching rules for satisfiability
• New methods for 3-SAT decision and worst-case analysis
• On a generalization of extended resolution
• Solving Satisfiability with Less Searching
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Power indices and easier hard problems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: New methods for 3-SAT decision and worst-case analysis