More Like this

1. On the Feasibility of High Throughput mmWave Backhaul Networks in Urban Areas

   https://doi.org/10.1109/ICNC47757.2020.9049824  

   Hu, Qiang; Blough, Douglas M. (February 2020, Proceedings of the International Conference on Computing, Networking and Communications)

   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
2. NNgSAT: Neural Network guided SAT Attack on Logic Locked Complex Structures

   Kimia Zamiri Azar, Hadi Mardani (November 2020, 2020 IEEE/ACM International Conference On Computer Aided Design (ICCAD))

   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
3. From Clauses to Klauses

   Reeves, Joseph E; Heule, Marijn; Bryant, Randal E (July 2024, International Conference on Computer Aided Verification (CAV-24))

   Satisfiability (SAT) solvers have been using the same input format for decades: a formula in conjunctive normal form. Cardinality constraints appear frequently in problem descriptions: over 64% of the SAT Competition formulas contain at least one cardinality constraint, while over 17% contain many large cardinality constraints. Allowing general cardinality constraints as input would simplify encodings and enable the solver to handle constraints natively or to encode them using different (and possibly dynamically changing) clausal forms. We modify the modern SAT solver CaDiCaL to handle cardinality constraints natively. Unlike the stronger cardinality reasoning in pseudo-Boolean (PB) or other systems, our incremental approach with cardinality-based propagation requires only moderate changes to a SAT solver, preserves the ability to run important inprocessing techniques, and is easily combined with existing proof-producing and validation tools. Our experimental evaluation on SAT Competition formulas shows our solver configurations with cardinality support consistently outperform other SAT and PB solvers. 

   more » « less
4. Clausal Proofs for Pseudo-Boolean Reasoning

   https://doi.org/10.1007/978-3-030-99524-9_25  

   Bryant, Randal E.; Heule, Marijn J. (January 2022, International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   Fisman, D.; Rosu, G. (Ed.)

   When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs. 

   more » « less
5. A New Constraint Satisfaction Perspective on Multi-Agent Path Finding: Preliminary Results

   Wang, J.; Li, J.; Ma, H.; Koenig, S.; Kumar, S. (January 2019, 18th International Conference on Autonomous Agents and Multi-Agent Systems)

   In this paper, we adopt a new perspective on the Multi-Agent Path Finding (MAPF) problem and view it as a Constraint Satisfaction Problem (CSP). A variable corresponds to an agent, its domain is the set of all paths from the start vertex to the goal vertex of the agent, and the constraints allow only conflict-free paths for each pair of agents. Although the domains and constraints are only implicitly defined, this new CSP perspective allows us to use successful techniques from CSP search. With the concomitant idea of using matrix computations for calculating the size of the reduced domain of an uninstantiated variable, we apply Dynamic Variable Ordering and Rapid Random Restarts to the MAPF problem. In our experiments, the resulting simple polynomial-time MAPF solver, called Matrix MAPF solver, either outperforms or matches the performance of many state-of-the-art solvers for the MAPF problem and its variants. 

   more » « less