Combinatorial auctions (CAs) have emerged as an important model in economics and show promise as a tool for resource allocation in AI. Unfortunately, winner determination for CAs is NP-hard and recent algorithms have difficulty with problems involving goods and bids beyond the hundreds. In this paper we apply a new stochastic local search algorithm, Casanova, to this problem. We demonstrate that it finds high quality (even optimal) solutions much faster than recently proposed methods (in many cases several orders of magnitude), particularly for large problems. In addition, we propose a logical language for naturally expressing combinatorial bids in which a single logical bid corresponds to a large (often exponential) number of explicit bids. We show that Casanova performs much better than systematic methods on such problems as well.