Parametric mechanism design via quantifier elimination

Abstract

This paper proposes an alternative automated mechanism design approach called parametric mechanism design via quantifier elimination (PMD-QE), which utilizes QE, a symbolic formula manipulation technique. In PMD-QE, we start from a skeleton of mechanisms, which is characterized by a set of parameters, e.g., critical values. The range of parameters where the given constraints are satisfied is automatically identified by QE. To demonstrate the potential of this idea, we are able to identify a non-trivial dominant-strategy incentive compatible mechanism for a setting where a bidder has a publicly known budget limit.