More Like this

1. Counting Knot Mosaics with ALLSAT (Student Abstract)

   https://doi.org/10.1609/AAAI.V37I13.27002  

   Miller, Hannah (June 2023, Proceedings of the AAAI Conference on Artificial Intelligence)

   Knot mosaics are a model of a quantum knot system. A knot mosaic is a m-by-n grid where each location on the grid may contain any of 11 possible tiles such that the final layout has closed loops. Oh et al. proved a recurrence relation of state matrices to count the number of m-by-n knot mosaics. Our contribution is to use ALLSAT solvers to count knot mosaics and to experimentally try different ways to encode the AT MOST ONE constraint in SAT. We plan to use our SAT method as a tool to list knot mosaics of interest for specific classes of knots. 

   more » « less
2. Long-lived metastable knots in polyampholyte chains

   https://doi.org/10.1371/journal.pone.0287200  

   Ozmaian, Masoumeh; Makarov, Dmitrii E. (June 2023, PLOS ONE)

   Yong, Xin (Ed.)

   Knots in proteins and DNA are known to have significant effect on their equilibrium and dynamic properties as well as on their function. While knot dynamics and thermodynamics in electrically neutral and uniformly charged polymer chains are relatively well understood, proteins are generally polyampholytes, with varied charge distributions along their backbones. Here we use simulations of knotted polymer chains to show that variation in the charge distribution on a polyampholyte chain with zero net charge leads to significant variation in the resulting knot dynamics, with some charge distributions resulting in long-lived metastable knots that escape the (open-ended) chain on a timescale that is much longer than that for knots in electrically neutral chains. The knot dynamics in such systems can be described, quantitatively, using a simple one-dimensional model where the knot undergoes biased Brownian motion along a “reaction coordinate”, equal to the knot size, in the presence of a potential of mean force. In this picture, long-lived knots result from charge sequences that create large electrostatic barriers to knot escape. This model allows us to predict knot lifetimes even when those times are not directly accessible by simulations. 

   more » « less
3. Fillable contact structures from positive surgery

   https://doi.org/10.1090/btran/200  

   Mark, Thomas; Tosun, Bülent (August 2024, Transactions of the American Mathematical Society, Series B)

   We consider the question of when the operation of contact surgery with positive surgery coefficient, along a knot $K$in a contact 3-manifold $Y$, gives rise to a weakly fillable contact structure. We show that this happens if and only if $Y$itself is weakly fillable, and $K$is isotopic to the boundary of a properly embedded symplectic disk inside a filling of $Y$. Moreover, if $Y^{\prime }$is a contact manifold arising from positive contact surgery along $K$, then any filling of $Y^{\prime }$is symplectomorphic to the complement of a suitable neighborhood of such a disk in a filling of $Y$. Using this result we deduce several necessary conditions for a knot in the standard 3-sphere to admit a fillable positive surgery, such as quasipositivity and equality between the slice genus and the 4-dimensional clasp number, and we give a characterization of such knots in terms of a quasipositive braid expression. We show that knots arising as the closure of a positive braid always admit a fillable positive surgery, as do knots that have lens space surgeries, and suitable satellites of such knots. In fact the majority of quasipositive knots with up to 10 crossings admit a fillable positive surgery. On the other hand, in general, (strong) quasipositivity, positivity, or Lagrangian fillability need not imply a knot admits a fillable positive contact surgery. 

   more » « less
4. The distribution of knots in the Petaluma model

   https://doi.org/10.2140/agt.2018.18.3647  

   Even-Zohar, C; Hass, J; Linial, N; Nowik, T (October 2018, Algebraic geometric topology)

   The representation of knots by petal diagrams (Adams et al 2012) naturally defines a sequence of distributions on the set of knots. We establish some basic properties of this randomized knot model. We prove that in the random n–petal model the probability of obtaining every specific knot type decays to zero as n, the number of petals, grows. In addition we improve the bounds relating the crossing number and the petal number of a knot. This implies that the n–petal model represents at least exponentially many distinct knots. Past approaches to showing, in some random models, that individual knot types occur with vanishing probability rely on the prevalence of localized connect summands as the complexity of the knot increases. However, this phenomenon is not clear in other models, including petal diagrams, random grid diagrams and uniform random polygons. Thus we provide a new approach to investigate this question. 

   more » « less
5. Verified Encodings for SAT Solvers

   Codel, Cayden; Avigad, Jeremy; Heule, Marijn J. (October 2023, Proceedings of the 23rd Conference on Formal Methods in Computer-Aided Design – FMCAD 2023)

   Nadel, Alexander; Rozier, Kristin Yvonne (Ed.)

   Satisfiability (SAT) solvers are versatile tools that can solve a wide array of problems, and the models and proofs of unsatisfiability emitted by SAT solvers can be checked by verified software. In this way, the SAT toolchain is trustworthy. However, many applications are not expressed natively in SAT and must instead be encoded into SAT. These encodings are often subtle, and implementations are error-prone. Formal correctness proofs are needed to ensure that implementations are bug-free. In this paper, we present a library for formally verifying SAT encodings, written using the Lean interactive theorem prover. Our library currently contains verified encodings for the parity, at-most-one, and at-most-k constraints. It also contains methods of generating fresh variable names and combining sub-encodings to form more complex ones, such as one for encoding a valid Sudoku board. The proofs in our library are general, and so this library serves as a basis for future encoding efforts. 

   more » « less