On the limit of branching rules for hard random unsatisfiable 3-SAT

DOI10.1016/S0166-218X(02)00408-0zbMath1029.68081MaRDI QIDQ1408384

Sylvain Gérard, Chu-Min Li

Publication date: 15 September 2003

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

zbMATH Keywords

SATDavis-Logemann-Loveland procedureBranching heuristicsMinimum search tree size

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items (1)

The state of SAT

Uses Software

• DIMACS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving propositional satisfiability problems
• A constraint-based approach to narrow search trees for satisfiability
• Branching rules for satisfiability
• On the complexity of choosing the branching literal in DPLL
• Experimental results on the crossover point in random 3-SAT
• Theory and Applications of Satisfiability Testing
• A machine program for theorem-proving
• Principles and Practice of Constraint Programming – CP 2003

This page was built for publication: On the limit of branching rules for hard random unsatisfiable 3-SAT