Three-valued logic solver? This is not my area, so apologizes if I am asking nonsense! 

I know that there are very good solver/theorem provers for solving 1st order logic. 

Now I have a problem, using 3-valued logic, but I am not sure if there are some practical ways of solving 3-valued logic (or converting it to a bigger 2-valued logic problem?)

EDIT1: Is it possible to translated (~reduce?) any 3-valued logic to 2-valued logic? Can this be generalized to K-valued logic, where K is any arbitrary integer? (What about the case when K is infinity?)

Any idea or reference is appreciated.
Let's assume that your three-valued logic consists of the truth values Yes, No and "unknown". We can think of these truth values as the sets $\{\top\}, \{\bot\}, \{\top,\bot\}$, and then the logical operations result in all possible values. For example, Yes and Unknown is Unknown while No and Unknown is No. 

A trick known as "double rail logic" uses two binary variables to represent each truth value: Yes is 1,1; No is 0,0; and Unknown is 1;0. The connectives And and Or are implemented using two matching gates, and Not by two negation gates followed by a swap. 

More generally, $k$-valued logic can be implemented by encoding each truth value using $\lceil\log_2 k\rceil$ bits. The logical operations are implemented using constant-size Boolean circuits. The advantage of the encoding above is that the circuits are very simple, in particular they read each input only once.