Abstract
Boolean satisfiability (SAT) is a well-studied N P-complete problem for formulating and solving other combinatorial problems like planning and scheduling. The Steiner tree problem (STP) asks to find a minimal cost tree in a graph that spans a set of nodes. STP has been shown to be N P-hard. In this paper, we propose to solve the STP by formulating it as a variation of SAT, and to solve it using a heuristic search method guided by the backbone of the problem. The algorithm is tested on a well known set of benchmark instances. Experimental results demonstrate the applicability of the proposed approach, and show that substantial quality improvement can be obtained compared to other heuristic methods.