Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
From MaRDI portal
Publication:5894155
DOI10.1613/jair.3152zbMath1214.68340MaRDI 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
68T05: Learning and adaptive systems in artificial intelligence
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Related Items
On Linear Resolution, On CDCL-Based Proof Systems with the Ordered Decision Strategy, New stochastic local search approaches for computing preferred extensions of abstract argumentation, Bounds on the size of PC and URC formulas, Narrow Proofs May Be Maximally Long, Constructing Hard Examples for Graph Isomorphism, Propositional proof complexity, Generating random instances of weighted model counting. An empirical analysis with varying primal treewidth, Are hitting formulas hard for resolution?, A note on SAT algorithms and proof complexity, Algorithms for computing minimal equivalent subformulas, A note about \(k\)-DNF resolution, What is answer set programming to propositional satisfiability, The complexity of proving that a graph is Ramsey, On dedicated CDCL strategies for PB solvers, Learning a propagation complete formula, Propositional proof systems based on maximum satisfiability, 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?, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, On Q-Resolution and CDCL QBF Solving, Knowledge Compilation with Empowerment, Space Complexity in Polynomial Calculus, An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances
Uses Software
