Creating a System of Boolean Equations, “Reverse Gaussian Elimination”

I have an idea for a game I'm developing where logic puzzles are randomly generated for the player to solve. For example:

A -> B
B -> C
A is ____
B is ____
C is false


...except the variables are replaced with random, absurd statements (IF Mr. Cuddles is fat, THEN the Dave Matthews Band is NOT a real band.)

My initial idea was to apply a modified "reverse Gaussian elimination" to a set of simple statements (A is true, B is false, etc) to complicate the problem, then remove a statement or two and let the user pick from a set of answers for the blank statements. Naturally, I figured if I could solve a system of logical equations using Gaussian-esque elimination, I could create one, so I'm trying to sort out the details of applying such a method. For example, I could construe the above as a matrix of linear equations, with M -> N converted to !M v N, ors construed as plusses, and 'k' as the constant factor/truth of each statement-- then, "add" the statements together to eliminate variables, like:

$\begin{bmatrix} A&B&C&k \\ f&t& &t \\ &f&t&t \\ & &f&t \end{bmatrix} -> \ \begin{bmatrix} A&B&C&k \\ f&t& &t \\ &f& &t \end{bmatrix} -> \ \begin{bmatrix} A&B&C&k \\ f& & &t \end{bmatrix}$

At least, the above works because !D v D is always true, and can thus be factored out. The problem is dealing with and, which basically makes the equations non-linear (since 'and'ing is comparable to multiplication). I'm also thinking you can never divide both sides by an 'anded' factor anyhow, since in order to do so, I believe you'd have to know the variable was non-zero (but then it'd have to be true, making the operation unnecessary to begin with.) My math education goes no further than Linear Algebra, unfortunately, so this is about where I get lost.

Similar to non-linear, single variable systems (matrices of equations like $x^2 + x + 1$), would it be possible to treat unique variable combinations as distinct variables, then deal with them after some elimination has been performed? Perhaps factor them out as separate statements, then invert them to be strings of 'or'ed, 'not'ed variables? Otherwise, is there a viable way of algorithmically (and thus randomly) creating such logical problems? Any reading material on the subject would also be greatly appreciated.

This if my first post here, so I'll be happy to clarify/improve this post in any way I can. Thanks!

-
 No answers or comments? Geez. – Philip Aug 5 '12 at 19:58