A limitation of the SAT approach to planning and the more recent Weighted-SAT approach to planning with preferences is the use of logical encodings where every fluent and action must be tagged with a time index. The result is that the complexity of the encodings grows exponentially with the planning horizon, and for metrics other than makespan, the optimality achieved is conditional on the planning horizon used. In this work, we consider the use of logical encodings in planning but for defining and computing admissible heuristics only, for which no time indices or planning horizons are required