And since I forgot to include them with my first tweet, (https://twitter.com/jix_/status/1336588447902011393) here are some figures to look at :) 15/15
I also have a small discord where I'm rambling about random things I'm working on, mostly SAT related stuff
if I know/follow you, feel free to DM me for an invite
(this isn't replacing twitter/mastodon for me. things I want to broadcast to everyone still end up here)
while I don't plan to leave twitter, since a while ago I'm also over at @jix in case anyone wants to follow me there
(I automatically mirror my tweets to mastodon, so apart from RTs and interactions it's the same content from my side)
I've also added support for it to the bitwuzla SMT solver (which already supports Kissat when incremental solving isn't required)
https://github.com/jix/bitwuzla/tree/kissat_extras
mostly to have a way to test things. what I plan to do with this will interface it directly and requires more patching
I've spent the last two weeks adding incremental solving to the Kissat SAT solver and just pushed a first public version of my patches to GitHub https://github.com/jix/kissat_extras
the stuff I changed hasn't seen much testing or performance tuning, but it seems to work fine so far
I came up with the following technique to emulate lifetime GATs on stable rust: https://gist.github.com/jix/42d0e4a36ace4c618a59f0ba03be5bf5 I haven't seen it before, and it works really well for my current use case (as well as the example in the gist). I'm curious, has anyone used or described this before?
An unconstructable still life in Conway's Game of Life: https://cp4space.hatsya.com/2022/01/14/conway-conjecture-settled/
The configuration shown in the link is stable (if its boundary is stabilized appropriately) but, if it appears in any pattern, it must always have been that way, in all predecessors of the pattern. As such, it answers the question "can every still life be constructed by gliders?" negatively.
also some limitations, e.g. just three channels, no per-channel parameters for anything but dense layers, no actual downsampling (but that can be emulated by adding lots of zeros to every matrix in later layers) ...
wonder what you could still do within those limitations
just realized you could implement (some) convolutional neural networks using SVG filters (https://developer.mozilla.org/en-US/docs/Web/SVG/Element/filter)
you've got feComponentTransfer for activation functions, feColorMatrix for dense layers, feConvolveMatrix for convolutions and feMorphology for max pooling ...
just transferring the cache hits to the worker, and only transferring the misses back to the cache certainly should end up storing and transferring a lot less data overall, but the extra roundtrips might hurt
but it's certainly significantly faster than not caching things
haven't compared the performance to github's actions/cache action caching ~/.cache/sccache, but caching complete snapshots of a LRU cache where both caches don't really know about each other just didn't feel right
on my quest for a CI setup for my rust projects that works more like I think it should, I added a GitHub Actions cache backend to sccache: https://github.com/jix/sccache
still experimental, needs more testing, but seems to work so far
(I still need to use something else to loop the audio back as a virtual input, it doesn't do that, but for that I already know working solutions on the platforms I use.)
I've wanted to use my phone as a transmitter for my lapel mic for a while. Using a cable long enough so I can walk over to the whiteboard tends to pick up noise and gets tangled up quickly. None of the many other apps I tried before worked, this one works perfectly.
Discovered a really nice piece of open source software today: SonoBus streams captured audio to other devices, with fairly low latency and importantly it runs on Linux, Windows, Mac, Android and iOS.
something very @SuricrasiaOnline : the "hash function crisis", where some academic comes out of nowhere breaking all commonly-used hash functions at once, even being able to find collisions *by hand* for one of them
this actually happened in 2005, where Wang broke MD2, MD4, MD5, RIPEMD, HAVAL, SHA-0, and a theoretical attack (which is now becoming practical) against SHA-1
Wang's paper was initially rejected for being completely incomprehensible, but then attended the related conference for that anyway, and gave a 10 minute unplanned talk where she demonstrated the attacks (including the by-hand collision finding for MD2)
So AFAICT, clingo/clasp only does preprocessing and no inprocessing. That makes adding literals on the fly during search easier to implement, but I really need merging of equivalent added literals. I guess this means, I'm back to waiting for me to get my own solver in shape
I also never seriously looked at what it'd take to add a custom theory to an SMT solver. Maybe I should do that at some point. From random bits of SMT solver code I've looked at, I think it's a bit more complex than clingo's propagator API though.
I have a few ideas that need this and every time I started hacking this into an existing SAT solver I ran into some obstacles that I found too annoying to work around. Eventually I want my own solver to be usable for this, but if I can try a few things before, that'd be great
LRT made me look at the clingo ASP solver, which wasn't really on my radar before. It seems to have a simple API for adding custom theory propagators, importantly it allows adding fresh literals on the fly. Might play around with it a bit tomorrow :) https://potassco.org/clingo/c-api/current/group__propagator