skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Chinese Remainder Encoding for Hamiltonian Cycles
The Hamiltonian Cycle Problem (HCP) consists of two constraints: i) each vertex contributes exactly two edges to the cycle; and ii) there is exactly one cycle. The former can be encoded naturally and compactly, while the encodings of the latter either lack arc consistency or require an exponential number of clauses. We present a new, small encoding for HCP based on the Chinese remainder theorem. We demonstrate the effectiveness of the encoding on challenging HCP instances.  more » « less
Award ID(s):
2006363
PAR ID:
10302525
Author(s) / Creator(s):
Date Published:
Journal Name:
Theory and Applications of Satisfiability Testing – SAT 2021
Volume:
12831
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Berg, Jeremias; Nordström, Jakob (Ed.)
    We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements. 
    more » « less
  2. Abstract Chinese hamster ovary (CHO) cells are among the most common cell lines used for therapeutic protein production. Membrane fouling during bioreactor harvesting is a major limitation for the downstream purification of therapeutic proteins. Host cell proteins (HCP) are the most challenging impurities during downstream purification processes. The present work focuses on identification of HCP foulants during CHO bioreactor harvesting using reverse asymmetrical commercial membrane BioOptimal™ MF‐SL. In order to investigate foulants and fouling behavior during cell clarification, for the first time a novel backwash process was developed to effectively elute almost all the HCP and DNA from the fouled membrane filter. The isoelectric points (pIs) and molecular weights (MWs) of major HCP in the bioreactor harvest and fouled on the membrane were successfully characterized using two‐dimensional gel electrophoresis (2D SDS‐PAGE). In addition, a total of 8 HCP were identified using matrix‐assisted laser desorption/ionization‐mass spectroscopy (MALDI‐MS). The majority of these HCP are enzymes or associated with exosomes, both of which can form submicron‐sized particles which could lead to the plugging of the filters. 
    more » « less
  3. The symmetric difference of two graphs on the same set of vertices is the graph on whose set of edges are all edges that belong to exactly one of the two graphs . For a fixed graph call a collection of spanning subgraphs of a connectivity code for if the symmetric difference of any two distinct subgraphs in is a connected spanning subgraph of . It is easy to see that the maximum possible cardinality of such a collection is at most , where is the edge‐connectivity of and is its minimum degree. We show that equality holds for any ‐regular (mild) expander, and observe that equality does not hold in several natural examples including any large cubic graph, the square of a long cycle and products of a small clique with a long cycle. 
    more » « less
  4. The seismic anisotropy of the Earth’s solid inner core has been the topic of much research. It could be explained by the crystallographic preferred orientation (CPO) developing during convection. The likely phase is hexagonal close-packed iron (hcp), alloyed with nickel and some lighter elements. Here we use high energy synchrotron X-rays to study CPO in Fe-9wt%Si, uniaxially compressed in a diamond anvil cell in radial geometry. The experiments reveal that strong preferred orientation forms in the low-pressure body-centred cubic (bcc) phase that appears to be softer than pure iron. CPO is attributed to dominant {110}<111>slip. The onset of the bcc→hcp transition occurs at a pressure of ≈15 GPa, and the alloy remains in a two phase bcc+hcp state up to 40 GPa. The hcp phase forms first with a distinct {11¯20} maximum perpendicular to compression. Modelling shows that this is a transformation texture, which can be described by Burgers orientation relationship with variant selection. Experimental results suggest that bcc grains oriented with <100> parallel to compression transform into hcp first. The CPO of the hcp changes only slowly during further pressure and deviatoric stress increase at ambient temperature. After heating to 1600 K, a change in the hcp CPO is observed with alignment of (0001) planes perpendicular to compression that can be interpreted as dominant (0001)<11¯20> slip, combined with {10¯12}<¯1011> mechanical twinning, which is similar to the deformation modes suggested previously for pure hcp iron at inner core conditions. 
    more » « less
  5. Bipartite graphs are a powerful tool for modeling the interactions between two distinct groups. These bipartite relationships often feature small, recurring structural patterns called motifs which are building blocks for community structure. One promising structure is the induced 6-cycle which consists of three nodes on each node set forming a cycle where each node has exactly two edges. In this paper, we study the problem of counting and utilizing induced 6-cycles in large bipartite networks. We first consider two adaptations inspired by previous works for cycle counting in bipartite networks. Then, we introduce a new approach for node triplets which offer a systematic way to count the induced 6-cycles, used in BATCHTRIPLETJOIN. Our experimental evaluation shows that BATCHTRIPLETJOIN is significantly faster than the other algorithms while being scalable to large graph sizes and number of cores. On a network with 112M edges, BATCHTRIPLETJOIN is able to finish the computation in 78 mins by using 52 threads. In addition, we provide a new way to identify anomalous node triplets by comparing and contrasting the butterfly and induced 6-cycle counts of the nodes. We showcase several case studies on real-world networks from Amazon Kindle ratings, Steam game reviews, and Yelp ratings. 
    more » « less