For the assignment problem where multiple indivisible items are allocated to a group of agents given their ordinal preferences, we design randomized mechanisms that satisfy first-choice maximality (FCM), i.e., maximizing the number of agents assigned their first choices, together with Pareto efficiency (PE). Our mechanisms also provide guarantees of ex-ante and ex-post fairness. The generalized eager Boston mechanism is ex-ante envy-free, and ex-post envy-free up to one item (EF1). The generalized probabilistic Boston mechanism is also ex-post EF1, and satisfies ex-ante efficiency instead of fairness. We also show that no strategyproof mechanism satisfies ex-post PE, EF1, and FCM simultaneously. In doing so, we expand the frontiers of simultaneously providing efficiency and both ex-ante and ex-post fairness guarantees for the assignment problem.

In the assignment problem, the goal is to assign indivisible items to agents who have ordinal preferences, efficiently and fairly, in a strategyproof manner. In practice, first-choice maximality, i.e., assigning a maximal number of agents their top items, is often identified as an important efficiency criterion and measure of agents' satisfaction. In this paper, we propose a natural and intuitive efficiency property, favoring-eagerness-for-remaining-items (FERI), which requires that each item is allocated to an agent who ranks it highest among remaining items, thereby implying first-choice maximality. Using FERI as a heuristic, we design mechanisms that satisfy ex-post or ex-ante variants of FERI together with combinations of other desirable properties of efficiency (Pareto-efficiency), fairness (strong equal treatment of equals and sd-weak-envy-freeness), and strategyproofness (sd-weak-strategyproofness). We also explore the limits of FERI mechanisms in providing stronger efficiency, fairness, or strategyproofness guarantees through impossibility results.

Separation logic and its variants can describe various properties on pointer programs. However, when it comes to properties on sequences, one may find it hard to formalize. To deal with properties on variable-length sequences and multilevel data structures, we propose sequence-heap separation logic which integrates sequences into logical reasoning on heap-manipulated programs. Quantifiers over sequence variables and singleton heap storing sequence (sequence singleton heap) are new members in our logic. Further, we study the satisfiability problem of two fragments. The propositional fragment of sequence-heap separation logic is decidable, and the fragment with 2 alternations on program variables and 1 alternation on sequence variables is undecidable. In addition, we explore boundaries between decidable and undecidable fragments of the logic with prenex normal form.

In the assignment problem, items must be assigned to agents who have unit demands, based on agents' ordinal preferences. Often the goal is to design a mechanism that is both fair and efficient. In this paper, we first prove that, unfortunately, the desirable efficiency notions rank-maximality, ex-post favoring-higher-ranks, and ex-ante favoring-higher-ranks, which aim to allocate each item to agents who rank it highest over all the items, are incompatible with the desirable fairness notions strong equal treatment of equals (SETE) and sd-weak-envy-freeness (sd-WEF) simultaneously. In light of this, we propose novel properties of efficiency based on a subtly different notion to favoring higher ranks, by favoring "eagerness" for remaining items and aiming to guarantee that each item is allocated to agents who rank it highest among remaining items. We prove that the eager Boston mechanism satisfies ep-FERI and sd-WSP, and that the uniform probabilistic respecting eagerness mechanism satisfies ea-FERI. We also prove that both mechanisms satisfy SETE and sd-WEF, and show that no mechanism can satisfy stronger versions of envyfreeness and strategyproofness while simultaneously maintaining SETE, and either ep-FERI or ea-FERI. X. Guo and Y. Cao are with Key Laboratory of High Confidence Software Technologies (MOE), Department of Computer Science and Technology, Peking University, Beijing 100871, China (e-mail: guoxiaoxi@pku.edu.cn; S. Sikdar is with Department of Computer Science, Binghamton University (email: ssikdar@binghamton.edu). H. Wang is with School of Computer Science and Cyber Engineering, Guangzhou University, China, and Key Laboratory of High Confidence Software Technologies (MOE), Department of Computer Science and Technology, Peking University, Beijing 100871, China (whpxhy@pku.edu.cn). This serves as a useful model for a variety of problems where the items may be either indivisible such as houses (Shapley and Scarf, 1974), dormitory rooms (Chen and Sönmez, 2002), and school choice without priorities (Miralles, 2009); or divisible such as natural resources like land and water (Segal-Halevi, 2016), and computational resources in cloud computing (Ghodsi et al., 2011, 2012; Grandl et al., 2014).

Partial preferences are natural in such problems since the number of bundles grows exponentially We propose multi-type probabilistic serial (MPS) with the number of types, and it is often unreasonable to expect and multi-type random priority (MRP) as extensions agents to form complete preferences over all bundles. of the well known PS and RP mechanisms Unfortunately, it is well known that no mechanism which to the multi-type resource allocation problem assigns each item fully to a single agent satisfies the basic (MTRA) with partial preferences. In our setting, fairness property of equal treatment of equals, meaning that there are multiple types of divisible items, everything else being equal, agents with the same preferences and a group of agents who have partial order should receive the same share of the resources. For example, preferences over bundles consisting of one item whenever two agents have equal and strict preferences over of each type. We show that for the unrestricted items, it is easy to see that no such mechanism satisfies equal domain of partial order preferences, no mechanism treatment of equals.