---
title: "A Structure-Based Variable Ordering Heuristic for SAT"
authors:
  - "Jinbo Huang"
  - "Adnan Darwiche"
doi: ""
url: "https://ijcai.org/proceedings/2003/166"
pdf: "https://ijcai.org/proceedings/2003/0166.pdf"
venue: "Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence"
year: 2003
pages: "1167-1171"
track: ""
keywords:
---

# A Structure-Based Variable Ordering Heuristic for SAT

Jinbo Huang, Adnan Darwiche

*Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence*, pages 1167-1171.

## Abstract

We propose a variable ordering heuristic for SAT, which is based on a structural analysis of the SAT problem. We show that when the heuristic is used by a Davis- Putnam SAT solver that employs conflict-directed backtracking, it produces a divide-and-conquer behavior in which the SAT problem is recursively decomposed into smaller problems that are solved independently. We discuss the implications of this divide-and-conquer behavior on our ability to provide structure-based guarantees on the complexity of Davis-Putnam SAT solvers. We also report on the integration of this heuristic with ZChaff-a state-of-the-art SAT solver-showing experimentally that it significantly improves performance on a range of benchmark problems that exhibit structure.