Limitations of restricted branching in clause learning

DOI10.1007/S10601-008-9062-ZzbMATH Open1192.68643OpenAlexW2177693862MaRDI QIDQ2272157FDOQ2272157

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

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

zbMATH Keywords

backdoor setsproof complexitypropositional satisfiabilityclause learningproblem structureDPLLbranching heuristics

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (10)

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

Uses Software

• MiniSat
• SAT competition
• Chaff
• BerkMin

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)