We consider a principal who periodically offers a fixed and costly nonmonetary reward to agents to incentivize them to invest effort over the long run. An agent’s output, as a function of his effort, is a priori uncertain and is worth a fixed per-unit value to the principal. The principal’s goal is to design an attractive reward policy that specifies how the rewards are to be given to an agent over time based on that agent’s past performance. This problem, which we denote by [Formula: see text], is motivated by practical examples from both academia (e.g., a reduced teaching load) and industry (e.g., “Supplier of the Year” awards). The following “limited-term” (LT) reward policy structure has been quite popular in practice. The principal evaluates each agent periodically; if an agent’s performance over a certain (limited) number of periods in the immediate past exceeds a predefined threshold, then the principal rewards him for a certain (limited) number of periods in the immediate future. When agents’ outputs are deterministic in their efforts, we show that there always exists an optimal policy that is an LT policy and also, obtain such a policy. When agents’ outputs are stochastic, we show that the class of LT policies may not contain any optimal policy of problem [Formula: see text] but is guaranteed to contain policies that are arbitrarily near optimal. Given any [Formula: see text], we show how to obtain an LT policy whose performance is within ϵ of that of an optimal policy. This guarantee depends crucially on the use of sufficiently long histories of the agents’ outputs. We also analyze LT policies with short histories and derive structural insights on the role played by (i) the length of the available history and (ii) the variability in the random variable governing an agent’s output. We show that the average performance of these policies is within 5% of the optimum, justifying their popularity in practice. We then introduce and analyze the class of “score-based” reward policies; we show that this class is guaranteed to contain an optimal policy and also, obtain such a policy. Finally, we analyze a generalization in which the principal has a limited number for rewards in any given period and show that the class of score-based policies, with modifications to accommodate the limited availability of the rewards, continues to contain an optimal solution for the principal. This paper was accepted by Jeannette Song, operations management. Supplemental Material: The online appendix is available at https://doi.org/10.1287/mnsc.2022.4482 .

Rosling (1989), one of the classic papers in inventory theory, studies an assembly system with stochastic demand. Under the condition that the initial state of the system possesses a certain property referred to as "long-run balance," the optimal policy is characterized as a balanced echelon base-stock policy. For the same model, we characterize the optimal policy starting with an arbitrary initial state, thereby completing the optimal policy description of Rosling (1989). The optimal policy is also a balanced echelon base-stock policy, but with dynamically evolving echelon base-stock levels. We also show that the policy prescribed by Rosling (1989) is still optimal, if the initial echelon inventory positions are non-decreasing in item index (items are indexed by their total lead time), which is a milder condition than the long-run balance condition and is easy to state and verify. In addition, for the two-component assembly system considered by Schmidt and Nahmias (1985), we show that the optimal policy is equivalent to a dynamic balanced echelon base-stock policy.

We consider a principal who periodically offers a fixed, binary, and costly non-monetary reward to agents endowed with private information, to incentivize the agents to invest effort over the long run. An agent's output, as a function of his effort, is a priori uncertain and is worth a fixed per-unit value to the principal. The principal's goal is to design an attractive reward policy that specifies how the rewards are to be given to an agent over time, based on that agent's past performance. This problem, which we denote by P, is motivated by practical examples from both academia (a reduced teaching load for achieving a certain research-productivity threshold) and industry ("Supplier of the Year" awards in recognition of excellent past performance). The following "limited-term'' reward policy structure has been quite popular in practice: The principal evaluates each agent periodically; if an agent's performance over a certain (limited) number of periods in the immediate past exceeds a pre-defined threshold, then the principal rewards him for a certain (limited) number of periods in the immediate future. For the deterministic special case of problem P, where there is no uncertainty in any agent's output given his effort, we show that there always exists an optimal policy that is a limited-term policy and also obtain such a policy. When agents' outputs are stochastic, we show that the class of limited-term policies may not contain any optimal policy of problem P but is guaranteed to contain policies that are arbitrarily near-optimal: Given any epsilon>0, we show how to obtain a limited-term policy whose performance is within epsilon of that of an optimal policy. This guarantee depends crucially on the use of sufficiently long histories of the agents' outputs for the determination of the rewards. In situations where access to this historical information is limited, we derive structural insights on the role played by (i) the length of the available history and (ii) the variability in the random variable governing an agent's output, on the performance of this class of policies. Finally, we introduce and analyze the class of "score-based'' reward policies - we show that this class is guaranteed to contain an optimal policy and also obtain such a policy.

We consider a firm that solicits bids from a fixed-sized pool of yet-to-be-qualified suppliers for an indivisible contract. The contract can only be awarded to a supplier who passes a multistage qualification process. For each stage of the qualification process, the buyer incurs a fixed testing cost for each supplier she chooses to test. The buyer seeks an optimal mechanism—that is, one that minimizes her total expected cost. Motivated by the buyer’s urgency (or the lack of it) of time for completing the qualification process, we obtain optimal mechanisms for two testing environments: (1) simultaneous testing, where in each stage, the buyer selects a subset of those suppliers who have passed all the previous stages and tests them simultaneously; and (2) nonsimultaneous testing, where the simultaneous-testing requirement is not imposed. Under simultaneous testing, the admission policy for selecting suppliers at each stage is based on nonuniform reserve-price thresholds. Under nonsimultaneous testing, too, the admission policy is threshold based, but the selection process is sequential in nature. The relative increase in cost due to the simultaneous-testing requirement is (under a mild condition) monotonically increasing in the number of suppliers, the expected multistage testing cost, and the overall passing probability. We also study the optimal sequencing of the qualification stages and show that the buyer should schedule the stages in increasing order of the ratio of their testing cost to their failing probability. Finally, for the simpler setting of a single-stage qualification process and a single supplier, we study a two-dimensional mechanism design problem where, in addition to cost, the passing probability is also private to the supplier. Here, too, threshold-based admission remains optimal, and the buyer offers either a pooling or a separating contract. The online appendix is available at https://doi.org/10.1287/msom.2017.0664 .

Descending mechanisms for procurement (or, ascending mechanisms for selling) have been well‐recognized for their simplicity from the viewpoint of bidders—they require less bidder sophistication as compared to sealed‐bid mechanisms. In this study, we consider procurement under each of two types of constraints: (1) Individual/Group Capacities: limitations on the amounts that can be sourced from individual and/or subsets of suppliers, and (2) Business Rules: lower and upper bounds on the number of suppliers to source from, and on the amount that can be sourced from any single supplier. We analyze two procurement problems, one that incorporates individual/group capacities and another that incorporates business rules. In each problem, we consider a buyer who wants to procure a fixed quantity of a product from a set of suppliers, where each supplier is endowed with a privately known constant marginal cost. The buyer's objective is to minimize her total expected procurement cost. For both problems, we present descending auction mechanisms that are optimal mechanisms. We then show that these two problems belong to a larger class of mechanism design problems with constraints specified by polymatroids, for which we prove that optimal mechanisms can be implemented as descending mechanisms.

We study fixed-dimensional stochastic dynamic programs in a discrete setting over a finite horizon. Under the primary assumption that the cost-to-go functions are discrete L♮-convex, we propose a pseudo-polynomial time approximation scheme that solves this problem to within an arbitrary prespecified additive error of ε > 0. The proposed approximation algorithm is a generalization of the explicit-enumeration algorithm and offers us full control in the trade-off between accuracy and running time. The main technique we develop for obtaining our scheme is approximation of a fixed-dimensional L♮-convex function on a bounded rectangular set, using only a selected number of points in its domain. Furthermore, we prove that the approximation function preserves L♮-convexity. Finally, to apply the approximate functions in a dynamic program, we bound the error propagation of the approximation. Our approximation scheme is illustrated on a well-known problem in inventory theory, the single-product problem with lost sales and lead times. We demonstrate the practical value of our scheme by implementing our approximation scheme and the explicit-enumeration algorithm on instances of this inventory problem.

We study several finite‐horizon, discrete‐time, dynamic, stochastic inventory control models with integer demands: the newsvendor model, its multi‐period extension, and a single‐product, multi‐echelon assembly model. Equivalent linear programs are formulated for the corresponding stochastic dynamic programs, and integrality results are derived based on the total unimodularity of the constraint matrices. Specifically, for all these models, starting with integer inventory levels, we show that there exist optimal policies that are integral. For the most general single‐product, multi‐echelon assembly system model, integrality results are also derived for a practical alternative to stochastic dynamic programming, namely, rolling‐horizon optimization by a similar argument. We also present a different approach to prove integrality results for stochastic inventory models. This new approach is based on a generalization we propose for the one‐dimensional notion of piecewise linearity with integer breakpoints to higher dimensions. The usefulness of this new approach is illustrated by establishing the integrality of both the dynamic programming and rolling‐horizon optimization models of a two‐product capacitated stochastic inventory control system.

(1) School of Information Science and Technology Beijing Forestry University China; (2) Naveen Jindal School of Management The University of Texas at Dallas United States; (3) College of Mathematics Physics and Information Engineering Zhejiang Normal University Jinhua China; (4) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences China

Consider the following "structured" procurement problem: A buyer wishes to procure a set of items (e.g., edges of a graph) from multiple suppliers, such that the procured items collectively form a basis of a matroid (e.g., a spanning tree of the graph). Each supplier is capable of supplying one item with a private cost. An item can have many competing suppliers. The goal is to minimize the buyer's expected cost. In this note, we propose a simple (in the sense that it is trivial for each supplier to determine her optimal bidding strategy) descending auction for this problem and prove its optimality.

In this paper, we propose an OBDD-based algorithm called greedy clique decomposition, which is a new variable grouping heuristic method, to solve difficult SAT problems. We implement our algorithm and compare it with several state-of-art SAT solvers including Minisat, Ebddres and TTS. We show that with this new heuristic method, our implementation of an OBDD-based satisfiability solver can perform better for selected difficult SAT problems, whose conflict graphs possess a clique-like structure.

Viewing OBDD from the explicit perspective of a propositional proof system is first proposed and studied in [A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77–91]. It has been shown that OBDD proof system defined in [A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77–91] is strictly stronger than resolution and can polynomially simulate cutting plane proof system with small coefficients CP∗. It is already shown in [W. Cook, C.R. Coullard, G. Turán, On the complexity of cutting-plane proofs, Discrete Appl. Math. 18 (1) (1987) 25–38] that there exists polynomial-size proof for pigeon hole problem PHPnn+1 of cutting plane proof system. Then it follows directly that there exists polynomial-size proof for PHPnn+1 of OBDD proof system. However, this is an indirect result. Atserias et al. [A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77–91] call for the need of a direct construction. Hereby we present such construction. Moreover, in this construction we do not need the weakening rule introduced in [A. Atserias, P.G. Kolaitis, M.Y. Vardi, Constraint propagation as a proof system, in: CP, 2004, pp. 77–91]. We believe this may shed some light on the understanding of the role of the weakening rule.

>SAT-based bounded model checking (BMC) has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic (LTL) formulae and then also adapted to check formulae of the universal fragment of computation tree logic (ACTL) by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an improved BMC approach for ACTL based on Penczek’s method. We consider two aspects of the approach. One is reduction of the number of variables and transitions in the k-model by distinguishing the temporal operator EX from the others. The other is simplification of the transformation of formulae by using uniform path encoding instead of a disjunction of all paths needed in the k-model. With these improvements, for an ACTL formula, the length of the final encoding of the formula in the worst case is reduced. The improved approach is implemented in the tool BMV and is compared with the original one by applying both to two well known examples, mutual exclusion and dining philosophers. The comparison shows the advantages of the improved approach with respect to the efficiency of model checking.

In this paper, we give a new and improved Bounded Model Checking encoding method for the universal fragment of CTL (ACTL). More specifically, the new encoding method works for verification of ACTL properties, instead of error-hunting. Combine our verification encoding and bug-hunting encoding proposed before, we get a Bounded Model Checking procedure that works for both valid and invalid ACTL properties. The underlying idea and intuition are summarized in this paper and we implement our tool BMV (Bounded Model Verification) on top of the well-known model checker NuSMV 2, and conduct experiments that show the strength and weakness of ACTL Bounded Model Checking compared to traditional BDD-based model checking procedure.