Solving with multiple assumptions

Suppose I have a CNF expression with variables (a,b,c,d,e,f,g). How would I go about using a SAT solver to find an assignment for (d,e,f) given that {a,b,c,g} = {1,0,0,1} and {a,b,c,g} = {1,1,1,1}? If it was one assumption, calling a sat solver to find assignments for {d,e,f} would be straight-forward (E.g., by adding unit clauses to the CNF). But what if I have multiple assumptions? Is this possible?

Here are the steps for what (I think) harold was trying to describe to you. You have some CNF formula F over the variables a, b, c, d, e, f and g.

1. Duplicate the formula, calling the duplicate G.
2. In G, replace the variable a with aa, b with bb, c with cc, and g with gg.
3. Add unit clauses to F so that (a,b,c,g) = (1,0,0,1).
4. Add unit clauses to G so that (aa,bb,cc,gg) = (1,1,1,1).
5. Concatenate the formulas F and G and feed the result into the SAT solver.

The solver will find a satisfying assignment consistent with both (a,b,c,g)'s and (aa,bb,cc,gg)'s preset values.