Solution robustness is a desirable feature when dealing with uncertainty. This issue has rarely been taken into account in the field of auctions, where the goal is to obtain optimal solutions (i.e., maximize the auctioneer's benefit). In this paper we define a notion of robustness for auctions where some resources may become unavailable once the auction has already been cleared. This notion of robustness balances the number of changes needed for repairing the solution and the possible loss of benefit for the auctioneer. In order to obtain robust solutions for auctions, we provide a mechanism based on transporting the concept of supermodel to the setting of weighted Max-SAT. We show that finding a supermodel of a weighted Max-SAT formula amounts to find a model of an SMT (Satisfiability Modulo Theories) formula.
Auctions are widely used as a resource allocation mechanism, since they enable an efficient distribution of resources amongst the agents requesting them [1]. Most auction mechanisms focus on maximizing the auctioneer's benefit, and assume that once the auction is cleared (i.e., a solution is found), the state of the world cannot change. However, in real applications, this is not the case. In the time between the clearance of the auction and the moment of the allocation of resources taking place, many things can happen. For instance, a machine that has been assigned to a given agent may break down before it starts using it, a winning agent may decide to withdraw its bid because it found a better deal elsewhere, etc. The consequence of such unexpected events is that the solution may then not yield the optimal benefits. Even worse, the solution may not be applicable at all. In such cases, a new solution must be found. To do so, the auction could be repeated, accounting for the new reality. However, the new solution could be completely different from the initial one, meaning that some Partially supported by the Spanish Ministry of Science and Innovation through the project SuRoS (ref. TIN2008-04547/TIN) bids that were winners in the first solution are losers in the new one. Such behavior could be a nuisance for the participating bidders, especially for those that were told their bids were winners but become losers in the repetition of the auction. To avoid such situations, the auctioneer could try to find a solution that is prepared for unexpected events. Ideally, such a solution should be applicable no matter what these events are, although this is not always achievable. Thus, when this happens, the solution should be reparable with the minimum number of changes to the original solution. And, while such a robust solution may be sub-optimal, we are interested in still obtaining a high revenue for the auctioneer.
The issue of bid withdrawal has already been addressed in [2]. But, as far as we know, the problem of resource unavailability has never been taken into account. Thus, in this paper we introduce a new mechanism for finding robust solutions to auctions with a bounded number of allowed breakages in resource availability, a bounded number of repairs in bid assignment, and a minimum guaranteed revenue for the auctioneer: If a solution is found, we can guarantee that, for any breakage in resource availability involving at most a resources, the solution can be repaired with at most b changes in bid assignment. In addition, the initial solution and all repaired solutions have a revenue of at least β. We call such a solution an (a,b,β)-super solution.
Our starting point is the standard modeling of an auction as a weighted Max-SAT problem [3,4] with boolean variables to denote whether a bid is winner or loser. In addition, we also use boolean variables representing resource availability. The transformation used to obtain (a, b, β)-super solutions works in the spirit of the one of [5] to obtain (a, b)-supermodels for propositional logic. As in [5], we define a set of breakable variables and a set of repairable variables. Here, the breakage set corresponds to the variables denoting resource availability, and the repair set to those corresponding to bid assignment.
In fact, our mechanism can be applied to any weighted Max-SAT problem, auctions being a particular case. An interesting aspect of our result is that weighted Max-SAT turns out to be not expressive enough to deal with the revenue constraints that we must add in the robust version of the problem. For this reason, we move to the setting of Satisfiability Modulo Theories (SMT) [6] and model the auction as a weighted Max-SMT formula. Hence, for our purposes the transformation of [5] must be adapted to this new setting.
The SMT problem for a theory T is: given a formula F , determine whether there is a model of T ∪ {F }. Hence, an SMT instance is a generalization of a boolean SAT instance in which some propositional variables have been replaced by predicates from the underlying theories. For example, if T denotes the theory of linear (integer or real) arithmetic, then a formula can contain clauses like, e.g., p ∨ q ∨ x + 2 ≤ y ∨ x = y + z, where p and q are boolean variables and x, y and z integer ones, providing a much richer modeling language than is possible with SAT formulas.
The rest of the paper is organized as follows. In Section 2 we review some related work concerning robustness and auctions. In Section 3 we formally define the kinds of auctions we consider. In Section 4 we describe an example to show how we look for robust solutions. Section 5 is devoted to the mechanism for finding robust solutions. Finally, in Section 6 we draw some conclusions and devise future work.
Here we briefly review some related work on robust solutions in general, and on robustness and the use of logics in the field of auctions.
The seminal work on robust solutions for propositional logic formulas is the one of [5], where the notion of supermodel is introduced. The complexity for finding such supermodels in several propositional logic fragments has been studied in [7].
Definition 1 (from [5]). An (S a 1 , S b 2 )-supermodel of a boolean formula F is a model of F such that if we modify the values taken by the variables in a subset of S 1 of size at most a (breakage), then another model can be obtained by modifying the values of the variables in a disjoint subset of S 2 of size at most b (repair).
An (S a 1 , S b 2 )-supermodel in which the breakage and the repair set are unrestricted is denoted as an (a, b)-supermodel.
The task of finding (a, b)-supermodels is NP-complete. The main idea is to encode the supermodel requirements of a formula F as a new formula F SM whose size is polynomially bounded by the size of F . This new formula F SM has a model if and only if F has an (a, b)-supermodel.
Example 1. The formula F = p ∨ q has three models, {p, q}, {¬p, q} and {p, ¬q}, which are all (1, 1)-supermodels. The encoding F SM for a (1, 1)-supermodel of F , according to [5], would be
Note that, for instance, if the satisfying interpretation (model) chosen for F SM is {¬p, q}, i.e., {p = false, q = true}, then p ∨ q is satisfied and, moreover, if q switches to false, then a new model for p ∨ q can be obtained by switching p to true. That is, a break in q has a repair on p. The key idea is that the value of the subformula ¬p ∨ ¬q under the initial interpretation coincides with the value of p ∨ q under the repaired interpretation and, hence, F SM has a model if and only if F has a supermodel. Note also that only the first model {p, q} is a (1, 0)-supermodel.
The concept of (a, b)-supermodel for propositional logic has been generalized to that of (a, b)-super solution in the context of constraint programming in [8].
There are several works that deal with robustness with respect to potential manipulations of the auction mechanism (such as false-name bids and other types of manipulations). However, this is not the concept of robustness we are interested in. As we have described in Section 1, we focus our research on robustness of the solution to the auction. Some works, such as [9,10] add the concept of robustness (fault tolerance) to mechanism desing in order to deal with potential failures in the execution of tasks by the agents, although they use a probabilistic approach and do not consider repairing the solutions. As far as we know, the only work that deals with solution repair in auctions is that of [2]. This work addresses the problem of bid withdrawal (i.e. a bidder that withdraws a winning bid), and, in order to find robust solutions, uses (α, β)-weighted super solutions [11], an extension of super solutions [8] that takes into account the breakage probability (α) and the cost of repair (β). Our work is similar, since our approach is also based on supermodels and we look for solutions with a bounded cost. However, we consider the problem of resource unavailability, which is not considered in [2]. Moreover, we are also interested in keeping the number of repairs low, which is only done indirectly (through the cost function) in [2]. In addition, our techniques are completely different because we use the logic framework of weighted Max-SAT and Satisfiability Modulo Theories, while [2] presents an ad-hoc search algorithm to find robust solutions.
Another closely related problem is that of robust knapsack [12] (i.e. a knapsack problem where the weights and/or values of the objects are imprecise). Given that many auction mechanisms can be modeled as a knapsack problem [13], it is reasonable to think that some of the robust approaches to this problem may yield robust solutions to auctions. However, the robustness concept used in the field of knapsack is somehow different to ours, since it does not consider the possibility of repairing a solution. Instead, a robust solution of a knapsack problem with imprecision is such that, on average, performs well regardless of what the actual weights or values of the objects are, in a similar way as the robustness presented in [9,10].
Regarding the use of logics in the field of auctions, it has been mainly used to define different bidding languages [14]. There are also some works that use logics as the method for solving the winner determination problem. For instance, Baral et al [15] model the auction using SModels, and use their approach to solve combinatorial auctions and combinatorial exchanges. However, they do not deal with robustness issues. On the other hand, modeling an auction as a weighted Max-SAT formula is a standard problem in Max-SAT benchmarks [4].
There are many types of auctions, depending on several factors, such as the number of items being offered, the number of units for each item, or the way in which bidders may express their requests, among others [16]. In this work, we restrict our attention to Combinatorial Auctions [17] and, more precisely, to the winner determination problem (clearing algorithm) of the auction. Formally, a combinatorial auction is defined as follows. There is:
a set of K agents, a set of N items or goods, and a set of M bids of the form (S i , p i ), where S i ⊆ {1..N } is the subset of goods (i.e. bundle) requested in bid i, and p i ∈ IR + is the value (price) of the bid. We denote by R j the set of indexes of the bids sent by agent j, j ∈ {1..K}.
The goal is to select the winning bids, so that no good is allocated more than once, and the revenue for the auctioneer is maximized:
where b i is a boolean variable indicating whether bid i is winner or loser.
Additionally, one may introduce other constraints, such as forcing all items to be allocated (which would imply replacing the ≤ of the previous equation by an equality), guaranteeing that all agents win at least (or at most) a given number of bids ( i∈Rj b i ≥ Q, ∀j ∈ {1..K}, where Q is the minimum number of winning bids per agent -or maximum if using ≤ Q), etc.
Regarding the bidding language, in the rest of the paper we assume that bidders use an OR-language [14], that is, each bidder submits a list of bids (pairs of bundle and price), and it is interested in winning any number of the bids sent to the auctioneer. However, the approach we present may work with any other bidding language (XOR, OR-of-XOR, . . . ), as long as the needed restrictions (as mentioned in the previous paragraph) are added.
In order to illustrate our approach, we present an example that we will use in the forthcoming sections to explain each of the steps needed to find robust solutions to auctions. For the sake of simplicity, we use single-item bundles, that is, each bid requests only one item. Moreover, we impose the constraint that each agent must win at least one of the bids it sent.
Example 2. Assume we have 3 agents and 4 goods (or resources). In the following table we indicate the price of each single-item bid of each agent:
We define the boolean variables g 1 , g 2 , g 3 and g 4 to represent the availability of the corresponding goods, and the boolean variables b i , i ∈ {1..7} to indicate whether bid i is winner or loser. Then, assuming that the only possible source of breakages is resource availability, we define the breakage set as being
a break in a resource may imply that a winning bid becomes loser and, eventually, other assignments can be reconsidered in order to improve the auctioneer's revenue under the new circumstances.
Assume that we look for robust solutions where one break may occur and each possible break must be repairable with at most four changes. Assume, moreover, that we want that whatever the break is, the revenue of the initial solution and of the repaired solution is at least 30. This will correspond to a (1, 4, 30)-super solution (see Definition 2 of Subsection 5.2).
The optimal solution to this auction without considering robustness would be to set as winning bids the second, the fourth, the fifth and the sixth bids, i.e.,
which means assigning good 2 to the first agent, goods 3 and 4 to the second agent and good 1 to the third agent. For the sake of readability we use the notation such as 2456 to indicate which are the winning bids of a solution. With this solution, the auctioneer would have a revenue of 60.
However, this optimal solution is not a (1, 4, 30)-super solution: if good 2 became unavailable (break), the only alternative for the first agent would be good 1, but this is already allocated to the third agent; this would imply finding also an alternative for the third agent, which would be good 4, but this good is allocated to the second agent. Thus, repairing the breakage of good 2 would imply modifying two winning bids (b 2 to b 1 and b 6 to b 7 ) and unassigning one winning bid (b 5 ), meaning five repairs (as shown in boldface):
which is more than the four allowed repairs. Note that for each bidder, choosing a new winning bid may imply two repairs (one to set the initially winning bid to 0, and in case he had no other winning bids, another one to set one of its losing bids to 1). This auction has 9 feasible solutions (i.e., solutions satisfying the constraints on bid incompatibility and minimum number of winning bids per agent), which are the following: 1247, 137, 1347, 147, 246, 2456, 247, 2467 and 256. Within these solutions, only three of them are (1, 4, 30)-super solutions: 246, 2467 and 247. Next we go through the details of solution 2467, i.e.,
which has a revenue of 50 units for the auctioneer. For this solution, the four possible breakages can be repaired as follows: It can be seen that all repairs have a revenue of at least 30 and the number of repairs is not greater than 4. Moreover, in the third case there is not even loss in the revenue. We let the reader check that solutions 246 and 247 are also (1,4,30)-super solutions, with a revenue of 40 and 35, respectively. However, since the revenue of solution 2467 is higher, this would be the optimal (1, 4, 30)super solution to this auction.
As for the rest of feasible solutions, some of them (147 and 1247) are (1, 4, )super solutions, meaning that they can be repaired with at most 4 changes, but not (1, 4, 30)-super solutions, since they do not satisfy that the solution and its repairs have a revenue of at least 30. In particular, solution 147 has a revenue of 30, but one of its repairs has a revenue of only 25 (when good 3 becomes unavailable, the second agent must be assigned good 2, which corresponds to a low value bid). Similarly, solution 1247 has a revenue of 45, but it also fails in the revenue of repairs, since one of them has again a revenue of 25.
Finally, some solutions (137, 1347, 2456 and 256) are not even (1, 4, )-super solutions, since they do need more than 4 changes in order to repair some of the breakages. This is the case of the optimal solution without robustness (2456), as we have seen a few paragraphs above.
An auction A as defined in Section 3 can be modeled as a weighted Max-SAT formula F A as follows. Let g 1 , . . . , g N be a set of boolean variables representing the availability of each of the N goods, and let b 1 , . . . , b M be a set of boolean variables representing whether each of the M bids is winner or loser.
1. Resource availability. For each bid j of the form (S j , p j ), where
to indicate that, whenever bid j is accepted, then all goods it requests must be available3 .
2. Bid incompatibility. For each pair of bids i and j (with i = j) such that S i ∩ S j = ∅, we state ¬b i ∨ ¬b j to indicate incompatibility between bids requesting the same good. 3. Minimum winning bids. For each set R k = {i 1 , . . . , i n k } corresponding to the bids of agent k, we state
to indicate that at least one bid of each agent must be accepted. Note that this restriction can change, or even disappear, depending on the type of bidding language used in the auction (OR, XOR, OR-of-XOR, . . . ) and also on the constraints about the number of winning bids per agent. 4. Bid's value. For each bid i, we add a unit clause
indicating that if bid i is not accepted, then there is a loss of revenue of p i .
The conjunction of the previous constraints defines a weighted Max-SAT problem for the auction.
Here we show how a weighted Max-SAT formula F A defining an auction A can be transformed into a weighted Max-SMT formula defining a robust version of the former. In particular, we describe how to obtain a Max-SMT formula F A SM such that F A SM has a model if and only if A has an (a, b, β)-super solution. Some of the proofs are omitted due to lack of space. Definition 2. An (a, b, β)-super solution of an auction is a (maximal revenue) solution for the auction such that, if a goods become unavailable (breakage), then another solution can be obtained by changing at most b bids from winner to loser or vice-versa (repair) and, moreover, the solution and all possible repaired solutions have a revenue of at least β.
The following definition generalizes the one of [5] to weighted Max-SAT. Definition 3. An (S a 1 , S b 2 , β)-supermodel of a weighted Max-SAT formula F is a model of F such that if we modify the values taken by the variables in a subset of S 1 of size at most a (breakage), another model can be obtained by modifying the values of the variables in a disjoint subset of S 2 of size at most b (repair) and, moreover, the solution and all possible repaired solutions have a cost of at most β. be a weighted Max-SAT formula, where C denotes the set of mandatory constraints and W denotes the set of weighted, non-mandatory constraints 4 . For the sake of simplicity, we will assume that W consists only of unary clauses of the form (b, w), where b is a boolean variable and w is a weight. Note that any Max-SAT formula can be transformed into an equisatisfiable one fulfilling this requirement by reification, i.e., by replacing any weighted constraint (G, w) such that G is not unary by (G ↔ b) ∧ (b, w). Now, assuming that
we introduce a set of integer variables i 1 , . . . , i k and define
Let S n denote the set of all (possibly empty) subsets of a set S whose size is at most n, and let S n+ denote the set of all non-empty subsets of a set S whose size is at most n. Moreover, let F S denote a boolean formula F where all occurrences of variables in the set S have been flipped (i.e., negated).
We define
where S is a set of boolean variables. We denote by B the particular case B ∅ = j∈1..k (1 − i j ) • w j , corresponding to the cost of the unsatisfied clauses in W . Finally, we define
Note that, due to L and the constraints of the form B ≤ β, this formula is not plain SAT: it falls into SAT modulo the quantifier-free fragment of the (first-order) linear arithmetic theory. The main lemma and theorem follow here. This lemma follows the spirit of the result of [5], but adding costs. Here, the key idea is that B S∪T , gives us the cost of the unsatisfied clauses in W if the variables in S ∪ T were to change their value with respect to the initial solution. Note that the variables in S represent the breakage variables and the ones in T represent the repair variables and, hence, S ∪ T denotes the set of variables that are going to change their value. Notice also that the sets S and T are disjoint, since it makes no sense to repair a broken variable.
Here we take the auction A of Example 2 and briefly describe how to model it as a robust auction. We begin by modeling the auction as a Max-SAT problem as explained in Subsection 5.1, which gives us
Note that S 1+ 1 denotes the non-empty subsets of S 1 with at most one element, i.e., the singletons {g 1 }, {g 2 }, {g 3 } and {g 4 }. And, since S 1 and S 2 are disjoint, we have that (S 2 \ S) 4 = S 4 2 , i.e., the (possibly empty) subsets of S 2 of size at most 4. Due to lack of space we do not develop C S∪T and B S∪T .
In this paper we have presented a mechanism for obtaining robust solutions to auctions. This issue has rarely been considered in the field of auctions, with only a few exceptions [2,9,10]. However, we think that robustness is a key issue when dealing with real world applications, where uncertainty is almost always present. In particular, we have focused on the possibility of some of the resources becoming unavailable once the auction has already been cleared. Thus, we provide a mechanism to proactively look for solutions that can be easily repaired when such unexpected events happen.
We have presented a notion of robustness that balances the number of allowed repairs when a break occurs and the loss of revenue for the auctioneer, by defining what we call (a, b, β)-super solutions. This allows the auctioneer to choose the more convenient values of each parameter, depending on how conservative or risk seeking its strategy is.
Our mechanism is based on the modeling of an auction as a weighted Max-SAT formula. However, since SAT does not allow to easily encode formulas with arithmetic operations, needed to achieve robustness, we have moved the problem to the richer logical framework of Satisfiability Modulo Theories.
Let us mention that state-of-the art SMT solvers have a rich input language, and it is not necessary (neither convenient) to translate any formula to CNF in order they can read it. In fact, we can feed an SMT solver directly with a formula such as F SM (as described in Subsection 5.2) contrarily to what is done in [5], where all formulas are translated to CNF. It is worth noting that we have not considered the option of translating our transformed formula into a linear program since, on the one hand, SMT solvers dealing with the theory of linear arithmetic already apply a (modified) simplex algorithm and, on the other hand, such a translation would imply a flattening of the structure of the problem (of which the SMT solvers can eventually take revenue) and the addition of many new variables. Moreover, the richness of the SMT language allows us to easily add new constraints when needed. Nevertheless, we have left as future work a peformance comparison with Operational Research tools.
Some experiments have been carried out with Yices [18], a weighted Max-SMT solver. At present only toy examples have been checked. In the future we plan to test our transformation with realistic benchmarks from the Combinatorial Auctions Test Suite (CATS) [19].
Finally, we want to acknowledge the fruitful discussions and comments we've had with the rest of the SuRoS project team.