A Structure-Based Variable Ordering Heuristic for SAT
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.
@inproceedings{ijcai2003p166,
title = {A Structure-Based Variable Ordering Heuristic for SAT},
author = {Huang, Jinbo and Darwiche, Adnan},
booktitle = {Proceedings of the Eighteenth International Joint Conference on
Artificial Intelligence, {IJCAI-03}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Georg Gottlob},
pages = {1167--1171},
year = {2003},
url = {https://ijcai.org/proceedings/2003/166},
}
TY - CPAPER TI - A Structure-Based Variable Ordering Heuristic for SAT AU - Huang, Jinbo AU - Darwiche, Adnan T2 - Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, IJCAI-03 PB - International Joint Conferences on Artificial Intelligence PY - 2003 SP - 1167 EP - 1171 UR - https://ijcai.org/proceedings/2003/166 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
