Find a binary matrix so that no vector from {-1,0,1}^n is in its kernel
I have a method for you that will help you find valid solutions (matrices) for many possible values of $m,n$.  However, it is not a complete answer to your question.  It can try to find a matrix for a particular value of $m,n$, but it might fail, and if it fails, you've learned nothing; my method cannot prove that no such matrix exists.
The method is based upon the following observation:
Theorem. If we have a valid $m_1\times n_1$ matrix $X_1$ that meets all your requirements (for parameters $m_1,n_1$) and a valid $m_2\times n_2$ matrix $X_2$ that meets all your requirements (for parameters $m_2,n_2$), then we can find a valid $m\times n$ matrix that meets all your requirements (for parameters $m,n$), where $m=m_1+m_2$ and $n=n_1+n_2$.
Proof.  Use the following matrix:
$$X = \begin{pmatrix} 0 &amp;X_1 \\ X_2 &amp;Z \end{pmatrix},$$
where $Z$ is arbitrary.  Suppose $Xy=0$, where $y \in \{-1,0,1\}^n$.  Then since the last $m_1$ coefficients of $Xy$ are zero, and since $X_1 y_1 =0$ implies $y_1=0$, it follows that the last $n_1$ coefficients of $y$ are zero.  Thus by letting $y_2$ be the restriction of $y$ to its first $m_2$ coefficients, we find that $X_2 y_2 = 0$.  But this implies $y_2 = 0$, i.e., $y=0$.  In other words, if $Xy=0$, then $y=0$.  This proves that $X$ is a valid matrix.

Now this lets us find many values of $m,n$ where it is possible to find a valid matrix $X$.  In particular, seed things with some small matrices for various small values of $m,n$ (using any convenient method); then you can derive some larger values of $m,n$ that also have such a matrix.
Here are some observations that will help you identify seed values $m,n$ where such a matrix $X$ exists:

First, a trivial observation: Obviously, if $n \le  m$, it is easy to find a valid solution $x$: just use the identity matrix (if $n&lt;m$, fill in the extra rows arbitrarily).  No need to use integer linear programming.  So this problem is only interesting when $n&gt;m$.

Second,  if $n$ is small enough, you can express this as a SAT instance and apply an off-the-shelf SAT solver.  The SAT instance will be of exponential size: it will have more than $3^n$ constraints, so this is only helpful for very small values of $n$, but it will still help you construct some values of $m,n$ where you can find a valid matrix $X$.

Third, you can use bcorso's answer to handle all cases where $n=m+1$ (there is always a valid solution, for $m\ge 3$).
In particular, you can construct a SAT instance where the $x_{i,j}$ are the variables.  Now, for each possible non-zero vector $y \in \{-1,0,1\}^n$, you can add a complicated constraint enforcing the requirement that $Xy \ne 0$.  (You'll need to have $m$ adders, each of which adds up to $n$ 0-or-1 values, and then a comparison to test whether the results of all of the $m$ adders are all zero or not.)


In this way, I would expect that, for each $n\le 8$ (or so), you can probably find the largest value of $m$ such that there exists a valid $m\times n$ matrix.  Now once you have those seed values, you can use the Theorem above to help you find additional values of $m,n$ where such a matrix exists.
As I stated above, this is not a complete solution, but it might help you solve your problem at least some of the time.

For general $m,n$, I doubt that there's any straightforward formulation of this as a polynomial-size integer linear program (unless $\text{NP} = \text{NP}^\text{co-NP}$ or the polynomial hierarchy collapses or something like that, which is not expected to hold; or unless you use some special knowledge about the solution to this problem).
Just telling whether a candidate value of $x$ is indeed a valid solution to this problem is $\text{co-NP}$-complete.  See https://cstheory.stackexchange.com/q/20277/5038.  In other, recognizing a solution to this problem can't be done in polynomial time (as far as we know); just recognizing a valid solution is $\text{co-NP}$-complete.  This means that the problem of finding a valid solution is in $\text{NP}^\text{co-NP}$.  In contrast, integer linear programming is in $\text{NP}$.  Therefore, without using some special knowledge about this problem, I don't think you can find a generic reduction from your problem to integer linear programming unless $\text{NP}^\text{co-NP} = \text{NP}$ (something that most complexity theorists believe is not likely to hold).
Don't take this too seriously.  I'm not trying to prove a formal theorem or anything like that; I'm just trying to give some weak evidence why this problem does not look like it has a straightforward, generic formulation as an instance of integer linear programming.
Of course, you can probably get a formulation as an integer linear program with a number of constraints that is exponential (say, in $m$), similar to how we got a SAT instance.  It'll be uglier, because expressing the constraint that some vector (namely, $Xy$) is not identically zero is ugly in ILP.  But it's doable.  See, e.g., Express boolean logic operations in zero-one integer linear programming (ILP).  However, I'm not sure this will be any better than the SAT-based method.  If I were implementing this, I would start by trying the SAT-based method, because (if you use a suitable front end, like STP) I think it will be easier to implement and might work just as well or better than an ILP-based formulation.