Is there a way to convert a program into a Boolean formula? Let's say I have a program P, in form of a binary code for x86 architecture. 

I want to find a Boolean formula F (in form of CNF, or something like that), such that

F(input,output) = true iff P(input) = output

So to answer a question "what output does the program produce on given input" I will only need to run a SAT/SMT solver for X on formula 

F(input,X) == true.

I understand that this problem is undecidable in general case, but I only care for some practical cases. 

What keywords should I google to find more about this topic?
Disclaimer: I'm not sure how useful any of this is for getting this done practically since you have a program, not a Turing Machine.

The Cook-Levin Theorem essentially states that you can translate the execution of a Turing Machine into a boolean formula that is polynomial in the length of the TM's execution such that the formula is satisfiable iff the TM accepts the input. 

In your case 'accepts' means 'returns true'. One could model this in a TM by transitioning to an accepting state instead of returning true.

The linked Wiki article gives a good exposition of the proof but the gist if it is that you have variables that describe the input to the machine, the sequence of states the machine takes during an execution, the position of the head during an execution, and a bunch of conjunctions that force satisfying assignment of the variables to describe a successful execution of the TM on the input.