The following pages link to (Q5715680):
Displaying 50 items.
- Projection, consistency, and George Boole (Q265702) (← links)
- Labelled interpolation systems for hyper-resolution, clausal, and local proofs (Q286731) (← links)
- Planning as satisfiability: heuristics (Q359984) (← links)
- Towards NP-P via proof complexity and search (Q408544) (← links)
- Learning from conflicts in propositional satisfiability (Q427560) (← links)
- A note on SAT algorithms and proof complexity (Q436581) (← links)
- Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search (Q457253) (← links)
- State space search nogood learning: online refinement of critical-path dead-end detectors in planning (Q514137) (← links)
- On the power of clause-learning SAT solvers as resolution engines (Q543613) (← links)
- Extended clause learning (Q622116) (← links)
- Producing and verifying extremely large propositional refutations (Q694550) (← links)
- Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT (Q764375) (← links)
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers (Q823775) (← links)
- Proof complexity of modal resolution (Q832717) (← links)
- A comparative runtime analysis of heuristic algorithms for satisfiability problems (Q835804) (← links)
- Formalization and implementation of modern SAT solvers (Q839035) (← links)
- Substitutions into propositional tautologies (Q845921) (← links)
- A generative power-law search tree model (Q1010292) (← links)
- \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver (Q1037644) (← links)
- Pool resolution is NP-hard to recognize (Q1042441) (← links)
- Constraint programming and operations research (Q1616390) (← links)
- Conflict-driven answer set solving: from theory to practice (Q1761291) (← links)
- Resolution cannot polynomially simulate compressed-BFS (Q1776193) (← links)
- Toward leaner binary-clause reasoning in a satisfiability solver (Q1777406) (← links)
- Resolution with counting: dag-like lower bounds and different moduli (Q2029775) (← links)
- Non-clausal redundancy properties (Q2055860) (← links)
- Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search (Q2074664) (← links)
- QBFFam: a tool for generating QBF families from proof complexity (Q2118282) (← links)
- Lower bounds for QCDCL via formula gauge (Q2118284) (← links)
- Propositional proof systems based on maximum satisfiability (Q2238728) (← links)
- Limitations of restricted branching in clause learning (Q2272157) (← links)
- Clause vivification by unit propagation in CDCL SAT solvers (Q2287199) (← links)
- Resolution over linear equations modulo two (Q2334112) (← links)
- A unified framework for DPLL(T) + certificates (Q2375732) (← links)
- A game characterisation of tree-like Q-resolution size (Q2424676) (← links)
- Constructive generation of very hard 3-colorability instances (Q2467358) (← links)
- What we can learn from conflicts in propositional satisfiability (Q2630816) (← links)
- The state of SAT (Q2643296) (← links)
- A simple proof of QBF hardness (Q2656352) (← links)
- Clause size reduction with all-UIP learning (Q2661332) (← links)
- Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space (Q2817796) (← links)
- Satisfiability via Smooth Pictures (Q2817998) (← links)
- Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers (Q2818010) (← links)
- On Q-Resolution and CDCL QBF Solving (Q2818030) (← links)
- DRAT Proofs for XOR Reasoning (Q2835888) (← links)
- Local consistency and SAT-solvers (Q2887073) (← links)
- An Expressive Model for Instance Decomposition Based Parallel SAT Solvers (Q2964456) (← links)
- Faster Extraction of High-Level Minimal Unsatisfiable Cores (Q3007682) (← links)
- On Freezing and Reactivating Learnt Clauses (Q3007683) (← links)
- Generalized Conflict-Clause Strengthening for Satisfiability Solvers (Q3007694) (← links)
