Zero forcing is a graph coloring process based on the following color change rule: all vertices of a graph [Formula: see text] are initially colored either blue or white; in each timestep, a white vertex turns blue if it is the only white neighbor of some blue vertex. A zero forcing set of [Formula: see text] is a set of blue vertices such that all vertices eventually become blue after iteratively applying the color change rule. The zero forcing number [Formula: see text] is the cardinality of a minimum zero forcing set. In this paper, we propose novel exact algorithms for computing [Formula: see text] based on formulating the zero forcing problem as a two-stage Boolean satisfiability problem. We also propose several heuristics for zero forcing based on iteratively adding blue vertices which color a large part of the remaining white vertices. These heuristics are used to speed up the exact algorithms and can also be of independent interest in approximating [Formula: see text]. Computational results on various types of graphs show that, in many cases, our algorithms offer a significant improvement on the state-of-the-art algorithms for zero forcing. Summary of Contribution: This paper proposes novel algorithms and heuristics for an NP-hard graph coloring problem that has numerous applications. Our exact methods combine Boolean satisfiability modeling with a constraint generation framework commonly used in operations research. The paper also includes an analysis of the facets of the polytope associated with this problem and decomposition techniques which can reduce the size of the problem. Our computational approaches are implemented and tested on a wide variety of graphs and are compared with the state-of-the-art algorithms from the literature. We show that our proposed algorithms based on Boolean satisfiability, in conjunction with the heuristics and order-reduction techniques, yield a significant speedup in some cases.
