  This paper proposes a Satisfiability Modulo Theory based formulation for
floorplanning in VLSI circuits. The proposed approach allows a number of fixed
blocks to be placed within a layout region without overlapping and at the same
time minimizing the area of the layout region. The proposed approach is
extended to allow a number of fixed blocks with ability to rotate and flexible
blocks (with variable width and height) to be placed within a layout without
overlap. Our target in all cases is reduction in area occupied on a chip which
is of vital importance in obtaining a good circuit design. Satisfiability
Modulo Theory combines the problem of Boolean satisfiability with domains such
as convex optimization. Satisfiability Modulo Theory provides a richer modeling
language than is possible with pure Boolean SAT formulas. We have conducted our
experiments on MCNC and GSRC benchmark circuits to calculate the total area
occupied, amount of deadspace and the total CPU time consumed while placing the
blocks without overlapping. The results obtained shows clearly that the amount
of dead space or wasted space is reduced if rotation is applied to the blocks.
