In this paper, we investigate the design of high throughput relay-assisted millimeter-wave (mmWave) backhaul networks in urban areas. Different from most related works, we consider the deployment of dedicated simple mmWave relay devices to help enhance the line-of-sight (LoS) connectivity of the backhaul network in urban areas with abundant obstacles. Given a set of (logical) backhaul links between base stations in the network, we propose an algorithm to find high-throughput LoS paths with relays for all logical links by minimizing interference within and between paths. We also propose methods to modify the backhaul topology to increase the probability of finding high-throughput paths using our algorithm. Extensive simulations, based on a 3-D model of a section of downtown Atlanta, demonstrate that high-throughput topologies, with minimal inter-path and intra-path interference, are feasible in most cases. The analyses also yield some insights on the mmWave backhaul network design problem.
more »
« less
Feasibility of Multipath Construction in mmWave Backhaul
This paper focuses on the problem of finding multiple paths with relay nodes to maximize throughput for ultra-high-rate millimeter wave (mmWave) backhaul networks in urban environments. Relays are selected between a pair of source and destination base stations to form multiple interference-free paths. We first formulate the problem of feasibility of multi-path construction as a constraint satisfaction problem that includes constraints on intra-path and inter-path interference and several other constraints that arise from the problem setting. Based on the derived equations, we transform the multiple paths construction problem into a Boolean satisfiability problem. This problem can then be solved through use of a satisfiability (SAT) solver, which however results in a very high running time for realistic problem sizes. To address this, we propose a heuristic algorithm that runs in a fraction of the time of the SAT solver and finds multiple interference-free paths using a modification of a maximum flow algorithm. Simulation results based on 3-D models of a section of downtown Atlanta show that the heuristic algorithm finds multiple paths in almost all the feasible cases (those where the SAT solver succeeds in finding a solution) and produces paths with higher average throughput than the SAT solver. Furthermore, the heuristic increases throughput by 50-100% in typical cases compared to a single-path solution.
more »
« less
- Award ID(s):
- 1813242
- NSF-PAR ID:
- 10322941
- Date Published:
- Journal Name:
- IEEE International Symposium on a World of Wireless, Mobile and Multimedia Networks
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
The globalization of the IC supply chain has raised many security threats, especially when untrusted parties are involved. This has created a demand for a dependable logic obfuscation solution to combat these threats. Amongst a wide range of threats and countermeasures on logic obfuscation in the 2010s decade, the Boolean satisfiability (SAT) attack, or one of its derivatives, could break almost all state-of-the-art logic obfuscation countermeasures. However, in some cases, particularly when the logic locked circuits contain complex structures, such as big multipliers, large routing networks, or big tree structures, the logic locked circuit is hard-to-be-solved for the SAT attack. Usage of these structures for obfuscation may lead a strong defense, as many SAT solvers fail to handle such complexity. However, in this paper, we propose a neural-network-guided SAT attack (NNgSAT), in which we examine the capability and effectiveness of a message-passing neural network (MPNN) for solving these complex structures (SAT-hard instances). In NNgSAT, after being trained as a classifier to predict SAT/UNSAT on a SAT problem (NN serves as a SAT solver), the neural network is used to guide/help the actual SAT solver for finding the SAT assignment(s). By training NN on conjunctive normal forms (CNFs) corresponded to a dataset of logic locked circuits, as well as fine-tuning the confidence rate of the NN prediction, our experiments show that NNgSAT could solve 93.5% of the logic locked circuits containing complex structures within a reasonable time, while the existing SAT attack cannot proceed the attack flow in them.more » « less
-
Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints to formulate a satisfiability query that is discharged with SAT or SMT solvers. The correctness of the evaluator is critical to the soundness of the tool and the domain properties it aims to guarantee. Yet so far, the trust in these evaluators has been based on an ad-hoc foundation of testing and manual reasoning. This paper presents the first formal framework for reasoning about the behavior of reusable symbolic evaluators. We develop a new symbolic semantics for these evaluators that incorporates state merging. Symbolic evaluators use state merging to avoid path explosion and generate compact encodings. To accommodate a wide range of implementations, our semantics is parameterized by a symbolic factory, which abstracts away the details of merging and creation of symbolic values. The semantics targets a rich language that extends Core Scheme with assumptions and assertions, and thus supports branching, loops, and (first-class) procedures. The semantics is designed to support reusability, by guaranteeing two key properties: legality of the generated symbolic states, and the reducibility of symbolic evaluation to concrete evaluation. Legality makes it simpler for client tools to formulate queries, and reducibility enables testing of client tools on concrete inputs. We use the Lean theorem prover to mechanize our symbolic semantics, prove that it is sound and complete with respect to the concrete semantics, and prove that it guarantees legality and reducibility. To demonstrate the generality of our semantics, we develop Leanette, a reference evaluator written in Lean, and Rosette 4, an optimized evaluator written in Racket. We prove Leanette correct with respect to the semantics, and validate Rosette 4 against Leanette via solver-aided differential testing. To demonstrate the practicality of our approach, we port 16 published verification and synthesis tools from Rosette 3 to Rosette 4. Rosette 3 is an existing reusable evaluator that implements the classic merging semantics, adopted from bounded model checking. Rosette 4 replaces the semantic core of Rosette 3 but keeps its optimized symbolic factory. Our results show that Rosette 4 matches the performance of Rosette 3 across a wide range of benchmarks, while providing a cleaner interface that simplifies the implementation of client tools.more » « less
-
We consider a variant of the Multi-Agent Path-Finding problem that seeks both task assignments and collision-free paths for a set of agents navigating on a graph, while minimizing the sum of costs of all agents. Our approach extends Conflict-Based Search (CBS), a framework that has been previously used to find collision-free paths for a given fixed task assignment. Our approach is based on two key ideas: (i) we operate on a search forest rather than a search tree; and (ii) we create the forest on demand, avoiding a factorial explosion of all possible task assignments. We show that our new algorithm, CBS-TA, is complete and optimal. The CBS framework allows us to extend our method to ECBS-TA, a bounded suboptimal version. We provide extensive empirical results comparing CBS-TA to task assignment followed by CBS, Conflict-Based Min-Cost-Flow (CBM), and an integer linear program (ILP) solution, demonstrating the advantages of our algorithm. Our results highlight a significant advantage in jointly optimizing the task assignment and path planning for very dense cases compared to the traditional method of solving those two problems independently. For large environments with many robots we show that the traditional approach is reasonable, but that we can achieve similar results with the same runtime but stronger suboptimality guarantees.more » « less
-
null (Ed.)Multi-Agent Path Finding (MAPF), i.e., finding collision-free paths for multiple robots, is important for many applications where small runtimes are necessary, including the kind of automated warehouses operated by Amazon. CBS is a lead- ing two-level search algorithm for solving MAPF optimally. ECBS is a bounded-suboptimal variant of CBS that uses focal search to speed up CBS by sacrificing optimality and instead guaranteeing that the costs of its solutions are within a given factor of optimal. In this paper, we study how to decrease its runtime even further using inadmissible heuristics. Motivated by Explicit Estimation Search (EES), we propose Explicit Estimation CBS (EECBS), a new bounded-suboptimal variant of CBS, that uses online learning to obtain inadmissible estimates of the cost of the solution of each high-level node and uses EES to choose which high-level node to expand next. We also investigate recent improvements of CBS and adapt them to EECBS. We find that EECBS with the improvements runs significantly faster than the state-of-the-art bounded-suboptimal MAPF algorithms ECBS, BCP-7, and eMDD-SAT on a variety of MAPF instances. We hope that the scalability of EECBS enables additional applications for bounded-suboptimal MAPF algorithms.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/WoWMoM51794.2021.00021
