Pinned post

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)

Show thread

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)

github.com/jix/bitwuzla/tree/k

mostly to have a way to test things. what I plan to do with this will interface it directly and requires more patching

Show thread

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 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: gist.github.com/jix/42d0e4a36a 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 -_-

An unconstructable still life in Conway's Game of Life: cp4space.hatsya.com/2022/01/14

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

Show thread

just realized you could implement (some) convolutional neural networks using SVG filters (developer.mozilla.org/en-US/do)

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

Show thread

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

Show thread

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: 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.)

Show thread

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.

Show thread

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.

sonobus.net/

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

Show thread

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.

Show thread

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

Show thread

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 :) potassco.org/clingo/c-api/curr

Show older
Mathstodon

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!