Pinned toot

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

Teaching multivariable calculus again for the first time in quite a while. Since this means teaching about the vector cross product, it brings to mind one the strangest "connection between wildly disparate-seeming things" theorems I know of:

prideout.net/blog/kauffman/

and part 2 of my "Proving 50-Year-Old Sorting Networks Optimal" series is out

it's a bit shorter than the first part and there is still a lot I haven't covered... but I wasn't getting anywhere before I decided to not put everything in this post

jix.one/proving-50-year-old-so

I'll post the source tomorrow after letting hopefully-less-tired-me review it once... will still be a mess though, need to clean it up another time, but it works, on some instances ridiculously well:

20M Nb51T6.cnf.xz
16K Nb51T6.cnfpack

Show thread

and then found a way that works really well for a lot of instances... it's basically delta encoding but where each literal can use one of the last 256 literals as base value for the delta, and distances and deltas are two separate streams...

Show thread

but zstd is pretty fast, so maybe I could use binary not ascii encoding, and maybe that works better with zstd... that got closer in size, but also opens up tons of possibilities like delta encoding etc so I spent a whole day just toying around with different ways to do that :D

Show thread

i was slightly annoyed at xz taking so long* to decompress larger problems... so I thought I'd recompress the instances using zstd... but it turns out that on cnf files, xz does a lot better than zstd and I didn't want to trade space for speed either...

*not really that long

Show thread

I want to have some better infrastructure for benchmarking my SAT solver ... and because I am very good at focusing on the important™ problems I wrote a packer for benchmark instances ^^
less than half the size of .xz and more than 4 times faster at unpacking sc2021 benchmarks

implemented minimization: github.com/jix/starlit/blob/46

I don't think I could've done that while streaming, at least not while also talking about what I'm doing

thinking about maybe doing summary streams instead, where I go over what I added since the last stream, but not sure yet...

Show thread

well that didn't go as planned

the implementation I did before isn't what I thought it was nor what I wanted to do now, and what I though it was didn't match the paper I thought it was described in ^^

and figuring a way out of that on stream apparently doesn't work for me

Show thread

today I want to add learned clause minimization to my SAT solver

plan is to start streaming in about an hour (~15:00 CEST)

youtu.be/7oWWPHrGqN4

Show thread

and another stream in a few minutes, plan is to add garbage collection to reclaim the space used by deleted clauses

youtu.be/rC-W9THpID0

Show thread

during the stream I talked about the 3-tiered clause database reduction strategy, but I forgot to actually mention the paper it's from: link.springer.com/chapter/10.1

Show thread

going to stream a bit again right now: youtu.be/zbRyjWVmxwY

didn't get around to glue computation yesterday, so the plan is to do that now

Show thread

streaming again in about an hour, plan is to add clause database reduction (including glue/LBD computation) to my new SAT solver

youtu.be/wxb2JEMAgpQ

Show thread
Show older
Mathstodon

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