Generating hard satisfiability problems

DOI10.1016/0004-3702(95)00045-3OpenAlexW2075335084WikidataQ56039657 ScholiaQ56039657MaRDI QIDQ2674174

Bart Selman, Hector J. Levesque, David G. Mitchell

Publication date: 22 September 2022

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(95)00045-3

zbMATH Keywords

phase transitionssatisfiabilityempirical studyrandom problems

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (38)

Generating Random SAT Instances: Multiple Solutions could be Predefined and Deeply Hidden ⋮ Nagging: A scalable fault-tolerant paradigm for distributed search ⋮ Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes ⋮ A sharp threshold in proof complexity yields lower bounds for satisfiability search ⋮ Implementing semantic merging operators using binary decision diagrams ⋮ Phase transitions of PP-complete satisfiability problems ⋮ A competitive and cooperative approach to propositional satisfiability ⋮ Satisfiability in Boolean Logic (SAT problem) is polynomial? ⋮ Complexity of Coloring Random Graphs ⋮ Some pitfalls for experimenters with random SAT ⋮ Generalized satisfiability problems: Minimal elements and phase transitions. ⋮ How to fake an RSA signature by encoding modular root finding as a SAT problem ⋮ A machine learning system to improve the performance of ASP solving based on encoding selection ⋮ Hierarchical Hardness Models for SAT ⋮ Unnamed Item ⋮ Experimental complexity analysis of continuous constraint satisfaction problems. ⋮ Fractional Edge Cover Number of Model RB ⋮ Partition-based logical reasoning for first-order and propositional theories ⋮ Compiling problem specifications into SAT ⋮ Satisfiability threshold for power law random 2-SAT in configuration model ⋮ A sharp threshold for the phase transition of a restricted satisfiability problem for Horn clauses ⋮ Measuring instance difficulty for combinatorial optimization problems ⋮ A new constraint test-case generator and the importance of hybrid optimizers ⋮ On SAT instance classes and a method for reliable performance experiments with SAT solvers ⋮ Algorithms for Effective Argumentation in Classical Propositional Logic: A Connection Graph Approach ⋮ Rigorous results for random (\(2+p)\)-SAT ⋮ Results related to threshold phenomena research in satisfiability: Lower bounds ⋮ New models for generating hard random Boolean formulas and disjunctive logic programs ⋮ An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses ⋮ A computational complexity analysis of tunable type inference for Generic Universe Types ⋮ Empirically-derived estimates of the complexity of labeling line drawings of polyhedral scenes ⋮ Remote Agent: to boldly go where no AI system has gone before ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ Backtracking algorithms for disjunctions of temporal constraints ⋮ On Super Strong ETH ⋮ On the complexity of unfrozen problems ⋮ Large hypertree width for sparse random hypergraphs ⋮ On the hierarchical community structure of practical Boolean formulas

Uses Software

• Walksat

Cites Work

• The intractability of resolution
• Resolution vs. cutting plane solution of inference problems: Some computational experience
• Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
• Solving the satisfiability problem by using randomized approach
• On the complexity of regular resolution and the Davis-Putnam procedure
• Easy problems are sometimes hard
• Branch-and-cut solution of inference problems in propositional logic
• Some pitfalls for experimenters with random SAT
• Critical behavior in the computational cost of satisfiability testing
• Critical Behavior in the Satisfiability of Random Boolean Expressions
• Many hard examples for resolution
• Outlier..........s
• A threshold for unsatisfiability
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Generating hard satisfiability problems