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
-
A complementary technique to decision-diagram-based model checking is SAT-based bounded model checking (BMC), which reduces the model checking problem to a propositional satisfiability problem so that the corresponding formula is satisfiable iff a counterexample or witness exists. Due to the branching time nature of computation tree logic (CTL), BMC for the universal fragment of CTL (ACTL) considers a counterexample in a bounded model as a set of bounded paths. Since the existential fragment of CTL (ECTL) is dual to ACTL, and ACTL formulas are often negated to obtain ECTL ones in practice, we focus on BMC for ECTL and propose an improved translation that generates a possibly smaller propositional formula by reducing the number of bounded paths to be considered in a witness. Experimental results show that the formulas generated by our approach are often easier for a SAT solver to answer. In addition, we propose a simple modification to the translation so that it is also defined for models with deadlock states.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1109/WoWMoM51794.2021.00021
