The last two-and-a-half decades have witnessed remarkable progress in
the development of decision procedures for various fragments of
first-order logic. One of the most powerful tools employed in this
area is the reduction of logical satisfiability problems to linear
programming or to linear integer programming. The purpose of this talk
is to survey some of the results that have been obtained in this way,
and to explain the connections between the structure of polyhedra and
the structure of models for the logical fragments in question.