Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
From MaRDI portal
Publication:5894155
DOI10.1613/jair.3152zbMath1214.68340OpenAlexW3103546459WikidataQ129519655 ScholiaQ129519655MaRDI QIDQ5894155
Marc Thurley, Albert Atserias, Johannes K. Fichte
Publication date: 8 March 2011
Published in: Journal of Artificial Intelligence Research (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1613/jair.3152
Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items (24)
Narrow Proofs May Be Maximally Long ⋮ Knowledge Compilation with Empowerment ⋮ A note about \(k\)-DNF resolution ⋮ Learning a propagation complete formula ⋮ Strong ETH and resolution via games and the multiplicity of strategies ⋮ Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all? ⋮ Space Complexity in Polynomial Calculus ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Generating random instances of weighted model counting. An empirical analysis with varying primal treewidth ⋮ Are hitting formulas hard for resolution? ⋮ What is answer set programming to propositional satisfiability ⋮ A note on SAT algorithms and proof complexity ⋮ The complexity of proving that a graph is Ramsey ⋮ Constructing Hard Examples for Graph Isomorphism ⋮ An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances ⋮ Algorithms for computing minimal equivalent subformulas ⋮ New stochastic local search approaches for computing preferred extensions of abstract argumentation ⋮ Bounds on the size of PC and URC formulas ⋮ Propositional proof systems based on maximum satisfiability ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Propositional proof complexity ⋮ On Linear Resolution ⋮ On dedicated CDCL strategies for PB solvers
Uses Software
This page was built for publication: Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
