assumptions: doc tweak
# UnSAT core extraction with assumption variables
-When a model is unsatisfiable, it can be desirable to get a better idea of which Boolean variables make it unsatisfiable. Commonly, these Boolean variables are 'switches' that turn constraints on and off, hence such Boolean variables can be used to get a better idea of which _constraints_ make the model unsatisfiable.
+When a model is unsatisfiable, it can be desirable to get a better idea of which Boolean variables make it unsatisfiable. Commonly, these Boolean variables are 'switches' that turn constraints on, hence such Boolean variables can be used to get a better idea of which _constraints_ make the model unsatisfiable.
-In the SATisfiability literature, the Boolean variables of interests are called _assumption_ variables. The subset of these variables that make the model unsatisfiable is called an unsatisfiable _core_.
+In the SATisfiability literature, the Boolean variables of interests are called _assumption_ variables and the solver will assume they are true. The subset of these variables that, when true, make the model unsatisfiable is called an unsatisfiable _core_.
Lazy Clause Generation solvers, like or-tools, are built on SAT solvers and hence can inherit the ability to define assumption variables and extract an unsatisfiable core.
