Jannis Harder @jix@mathstodon.xyz

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?

maybe I shouldn't software anymore for today ...

ran into a rustc ICE and while I was writing an issue for it, firefox crashed on me -_-

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.

https://www.sonobus.net/

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