Pinned toot

Just published the first in a series of blog posts about my recent-ish sorting network result. In it I introduce the problem and summarize the previous state of the art:

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

Watched another talk. This one by Moshe Vardi is about looking beyond the CDCL monoculture, using BDD based approaches as example.

youtu.be/fmgj85emb4s

Show thread

Internally it's a predictive recursive descent parser, so it's much easier to extend than the hand rolled state machine I was using before and it also happens to be faster. I'm not using any existing parsing libs as I didn't find one that supported everything I wanted.

Show thread

Published a rust crate to efficiently parse and write DIMACS CNF: crates.io/crates/flussab-cnf. I also plan to eventually add support for extensions and related formats as I need them, e.g. xor clauses, WCNF, QDIMACS, DRAT, etc.

ideally devices would recalibrate the gauge total whenever the battery goes empty, but often that doesn't seem to work in practice, giving you the issues that prompted this. (empty and full can be detected via measurement, only in between is difficult afaiui.)

Show thread

either this is not as funny (that's ok :D) or "battery fuel gauge" is more obscure than I thought it is (also ok, but knowing how displayed charge % is mostly not directly measured, but dead reckoned by integrating (dis)charge current via a "fuel gauge" circuit is useful imo)

Show thread

friend's laptop battery cut out during a video call while supposedly still having 12% charge left...

battery fuel gauge? more like battery fuels rage!

currently writing some code that allocates a buffer that is always at least fixed amount larger than what's used, so code that processes the data can use faster imprecise/deferred end-of-buffer checks (like e.g. in fgiesen.wordpress.com/2016/01/)

const BONUS_DATA_LEN: usize = 64;

The new placement of the docs.rs link for crates on crates.io trips me up... but since I learned how to write user scripts recently, I wrote one that adds a hotkey for it: gist.github.com/jix/f0cb842d4f

Now I just need to press d to get to the docs :)

There also seem to be seminar talks not on youtube (yet?), but thankfully Mate Soos tweeted a link to the video of his talk on implementing efficient propagation, reason generation and backtracking with XOR constraints when solving CNF-XOR formulas:

twitter.com/SoosMate/status/13

Show thread

A talk on verifying optimized multiplier circuits by combining SAT solving with computer algebra (specifically Gröbner bases, using the structure of the problem to make their computation feasible) by Daniela Kaufmann (@DanielaKaufmann@twitter.com)

youtu.be/OhHqpHUamCI

Show thread

An introduction to approximate counting and sampling of solutions to SAT instances by Kuldeep S. Meel (@ksmeel@twitter.com)

youtu.be/49A6E_Yd0ow

Also a second talk with more details (it's a self-contained talk so there is some overlap)

youtu.be/aQcVdFYIEpI

youtu.be/49A6E_Yd0ow

Show thread

A 4 part tutorial on solving and optimizing with Pseudo-Boolean constraints (linear constraints over Boolean variables) by Jakob Nordström

youtu.be/f8d9VxONa0E (Part 1)
youtu.be/aihmjopvuZQ (Part 2)
youtu.be/6VW1fsTYZcg (Part 3)
youtu.be/1_nd_Di4Vts (Part 4)

Show thread

Currently there are a lot of great talks about SAT solving and related topics appearing on the Simons Institute youtube channel: youtube.com/c/SimonsInstitute/

I'll use this thread to post links to the ones I've watched:

Only tested on firefox with violentmonkey. If other browsers/extensions need fixes I can add them (but I won't test that myself).

The overall approach should also be quite robust against twitter randomly changing things... I'm not making any assumptions about the DOM structure.

Show thread

I often copy links from twitter, so I'm quite annoyed by t.co URLs. Finally wrote a simple userscript to resolve them so I can just right click to copy them: gist.github.com/jix/e67c127820

Didn't want to trust any of the super complicated existing ones I found…

Would be nice to have this as a cargo subcommand written in rust, also with better handling of the diagnostics output by rustdoc, but this hack only took a few minutes to write when I was annoyed of having too many open browser tabs with stale versions of my docs again

Show thread

A while ago I wrote a small hacky script to auto run `cargo doc` on source changes and to also serve the resulting docs locally using livereload so I don't need to refresh open browser tabs: gist.github.com/jix/caf2d46ceb

Maybe I'm not the only one who finds this helpful :)

The new vscode "wrap tabs" option (code.visualstudio.com/updates/) sounds like something I need. I navigate a lot using the tab bar, always leave open too many files, and get annoyed if I don't see the one I want to switch to. Let's see if this helps or if I'll drown in stacked tabs ^^

Show older
Mathstodon

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