---
title: "A backbone-search heuristic for efficient solving of hard 3-SAT formulae"
authors:
  - "Olivier Dubois"
  - "Gilles Dequen"
doi: ""
url: "https://ijcai.org/proceedings/2001/35"
pdf: "https://ijcai.org/proceedings/2001/0035.pdf"
venue: "Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence"
year: 2001
pages: "248-252"
track: ""
keywords:
---

# A backbone-search heuristic for efficient solving of hard 3-SAT formulae

Olivier Dubois, Gilles Dequen

*Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence*, pages 248-252.

## Abstract

Of late, new insight into the study of random -SAT formulae has been gained from the introduction of a concept inspired by models of physics, the ‘backbone’ of a SAT formula which corresponds to the variables having a fixed truth value in all assignments satisfying the maximum number of clauses. In the present paper, we show that this concept, already invaluable from a theoretical viewpoint in the study of the satisfiability transition, can also play an important role in the design of efficient DPL-type algorithms for solving hard random -SAT formulae and more specifically -SAT formulae. We define a heuristic search for variables belonging to the backbone of a -SAT formula which are chosen as branch nodes for the tree developed by a DPL-type procedure. We give in addition a simple technique to magnify the effect of the heuristic. Implementation yields DPL-type algorithms with a significant performance improvement over the best current algorithms, making it possible to handle unsatisfiable hard 3-SAT formulae up to 700 variables.