Rational points on varieties over local fields In his expanded lecture notes Rational points on varieties, Bjorn Poonen writes the following:

REMARK 2.5.3: There is an algorithm that, given a local field $k$ of characteristic $0$ and a $k$-variety $X$, decides whether $X(k)$ is nonempty. (...)

I would like to see if this algorithm can be applied to determine the existence of rational points on a very specific family of varieties over $\mathbb{Q}_p$. Unfortunately, I could not find anything related on the web so far. Could you point to some literature on this matter, or explain some of the ideas?
 A: Let us assume that $X$ is smooth and projective for simplicity, given by a
number of polynomial equations with coefficients in the ring of integers
$\mathcal O$ of $k$. Let $\kappa$ denote the residue class field of $k$.
Reduce the equation moduloe the maximal ideal to get the reduced variety
$\bar X$. Enumerate the $\kappa$-points of $\bar X$ (this is a finite
problem). If $\bar X(\kappa) = \emptyset$, then $X(k)$ is empty.
If there is a smooth point $\bar P \in \bar X(\kappa)$
(and $\dim \bar X = \dim X$), then it lifts by Hensel's Lemma to a point
on $X(k)$, so $X(k)$ is non-empty. Otherwise, consider the lifts of
each point to points modulo the square of the maximal ideal. This comes
down to looking at equations $f(\dots, a_i + \pi x_i, \dots)$,
where $f$ runs through the equations defining an affine patch of $X$
containing a lift of $\bar P$, $a_i$ are lifts
of the coordinates of $\bar P$ and $x_i$ are variables; divide the equations
by the highest possible power of $\pi$, which is a generator of the
maximal ideal, and reduce mod $\pi$. This gives equations for the reduction
mod $\pi$ of a different model of $X$. Smoothness of $X$ guarantees
that the process will terminate after finitely many lifting steps.
If $X$ is not smooth, consider its singular locus $X'$ first (recursively).
If $X'(k)$ is non-empty, so is $X(k)$. Otherwise, run the previous
procedure on $X$. Since $X'(k)$ is empty, all points that lift indefinitely
will end up on the smooth part of $X$, which again gives termination.
Magma has an implementation (IsLocallySoluble). See
Nils Bruin, Some ternary Diophantine equations of signature (n, n, 2),
In Bosma and Cannon, Discovering Mathematics with Magma,
Springer-Verlag, Heidelberg, 2004. 
