Limitations of restricted branching in clause learning

DOI10.1007/S10601-008-9062-ZMaRDI QIDQ2272157zbMATH OpenOpenAlexFDO

Authors Matti Järvisalo, Tommi Junttila

Publication date 6 August 2009

Published in Constraints (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10601-008-9062-z

zbMATH Keywords

backdoor setsbranching heuristicsclause learningDPLLproblem structureproof complexitypropositional satisfiability

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Limitations of Restricted Branching in Clause Learning
• The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study
• scientific article; zbMATH DE number 2243370
• Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• A sharp threshold in proof complexity yields lower bounds for satisfiability search
• An exponential separation between regular and general resolution
• BMC via on-the-fly determinization
• Exponential bounds for DPLL below the satisfiability threshold
• Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas
• Formal Methods in Computer-Aided Design
• Hard examples for resolution
• Hard satisfiable instances for DPLL-type algorithms
• scientific article; zbMATH DE number 1670796 (Why is no real title available?)
• scientific article; zbMATH DE number 1696820 (Why is no real title available?)
• scientific article; zbMATH DE number 3888913 (Why is no real title available?)
• scientific article; zbMATH DE number 1796153 (Why is no real title available?)
• scientific article; zbMATH DE number 1931668 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Limitations of Restricted Branching in Clause Learning
• Many hard examples for resolution
• Mutilated chessboard problem is exponentially hard for resolution
• Principles and Practice of Constraint Programming – CP 2004
• Regular Resolution Versus Unrestricted Resolution
• The Complexity of Propositional Proofs
• The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study
• The efficiency of resolution and Davis-Putnam procedures
• The intractability of resolution
• The relative efficiency of propositional proof systems
• The resolution complexity of independent sets and vertex covers in random graphs
• The resolution complexity of random graph \(k\)-colorability
• Theory and Applications of Satisfiability Testing
• Unrestricted vs restricted cut in a tableau method for Boolean circuits

Cited in

(10)

• Propagation complete encodings of smooth DNNF theories
• Backdoors to tractable answer set programming
• Algorithms for Solving Satisfiability Problems with Qualitative Preferences
• DPLL+ROBDD derivation applied to inversion of some cryptographic functions
• Limitations of Restricted Branching in Clause Learning
• Planning as satisfiability: heuristics
• An Exponential Lower Bound for Width-Restricted Clause Learning
• On exponential lower bounds for partially ordered resolution
• scientific article; zbMATH DE number 7199588 (Why is no real title available?)
• Finding Effective SAT Partitionings Via Black-Box Optimization

Describes a project that uses

Uses Software

• MiniSat
• Chaff
• BerkMin
• SAT competition

This page was built for publication: Limitations of restricted branching in clause learning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2272157)