scientific article; zbMATH DE number 2243370

zbMath1080.68651arXiv1107.0044MaRDI QIDQ5715680

Ashish Sabharwal, Henry A. Kautz, P. W. Beame

Publication date: 4 January 2006

Full work available at URL: https://arxiv.org/abs/1107.0044

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).

Related Items (68)

Projection, consistency, and George Boole ⋮ Constraint programming and operations research ⋮ On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Proof complexity of modal resolution ⋮ A comparative runtime analysis of heuristic algorithms for satisfiability problems ⋮ Formalization and implementation of modern SAT solvers ⋮ A unified framework for DPLL(T) + certificates ⋮ Hints Revealed ⋮ Evaluating CDCL Variable Scoring Schemes ⋮ Substitutions into propositional tautologies ⋮ The state of SAT ⋮ A simple proof of QBF hardness ⋮ Planning as satisfiability: heuristics ⋮ On CDCL-Based Proof Systems with the Ordered Decision Strategy ⋮ Unnamed Item ⋮ A Generalized Framework for Conflict Analysis ⋮ Extended clause learning ⋮ Towards NP-P via proof complexity and search ⋮ A game characterisation of tree-like Q-resolution size ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Are hitting formulas hard for resolution? ⋮ An Expressive Model for Instance Decomposition Based Parallel SAT Solvers ⋮ A note on SAT algorithms and proof complexity ⋮ Limitations of Restricted Branching in Clause Learning ⋮ Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search ⋮ Logic-Based Benders Decomposition for Large-Scale Optimization ⋮ DPLL: The Core of Modern Satisfiability Solvers ⋮ Faster Extraction of High-Level Minimal Unsatisfiable Cores ⋮ On Freezing and Reactivating Learnt Clauses ⋮ Generalized Conflict-Clause Strengthening for Satisfiability Solvers ⋮ Empirical Study of the Anatomy of Modern Sat Solvers ⋮ Propositional proof systems based on maximum satisfiability ⋮ Constructive generation of very hard 3-colorability instances ⋮ State space search nogood learning: online refinement of critical-path dead-end detectors in planning ⋮ Producing and verifying extremely large propositional refutations ⋮ Conflict-driven answer set solving: from theory to practice ⋮ On the power of clause-learning SAT solvers as resolution engines ⋮ Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases ⋮ Lower bounds for QCDCL via formula gauge ⋮ Unnamed Item ⋮ Resolution cannot polynomially simulate compressed-BFS ⋮ Limitations of restricted branching in clause learning ⋮ Resolution with counting: dag-like lower bounds and different moduli ⋮ Clause vivification by unit propagation in CDCL SAT solvers ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ A generative power-law search tree model ⋮ Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space ⋮ Satisfiability via Smooth Pictures ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Propositional proof complexity ⋮ Non-clausal redundancy properties ⋮ Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ Some applications of propositional logic to cellular automata ⋮ DRAT Proofs for XOR Reasoning ⋮ Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search ⋮ \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver ⋮ Pool resolution is NP-hard to recognize ⋮ Unnamed Item ⋮ Present and Future of Practical SAT Solving ⋮ Resolution over linear equations modulo two ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores ⋮ On Exponential Lower Bounds for Partially Ordered Resolution ⋮ On Linear Resolution ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge

Uses Software

This page was built for publication: