ECAI-2000 Logo

ECAI-2000 Conference Paper

[PDF] [full paper] [prev] [tofc] [next]

On the Limit of Branching Rules for Hard Random Unsatisfiable 3-SAT

Chu Min Li, Sylvain Gérard

We study the limit of branching rules in Davis-Putnam (DP) procedure for hard random unsatisfiable 3-SAT and try to answer the question: what would be the search tree size if every branching variable were the best possible? The issue is of practical interest because many efforts have been spent for designing better branching rules. Our experimental results suggest that the branching rules used in the current state-of-the-art DP procedures are already close to the optimal, and in particular, that the first of the ten IJCAI-97 challenges for propositional reasoning and search formulated by Selman et al., namely, proving a hard 700 variable random 3-SAT formula is unsatisfiable, probably cannot be answered by DP procedure unless something significantly different from branching can be made effective for hard random unsatisfiable 3-SAT

Keywords: Search, Constraint Satisfaction, Automated Reasoning, Theorem Proving, Branching, Davis-Putnam Procedure, SAT

Citation: Chu Min Li, Sylvain Gérard: On the Limit of Branching Rules for Hard Random Unsatisfiable 3-SAT. In W.Horn (ed.): ECAI2000, Proceedings of the 14th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2000, pp.98-102.

[prev] [tofc] [next]

ECAI-2000 is organised by the European Coordinating Committee for Artificial Intelligence (ECCAI) and hosted by the Humboldt University on behalf of Gesellschaft für Informatik.