Jannis Harder @jix@mathstodon.xyz
- Website
- https://jix.one
- https://twitter.com/jix_
Joined Aug 2020
Pinned toot
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
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:
https://jix.one/proving-50-year-old-sorting-networks-optimal-part-1/
Watched another talk. This one by Moshe Vardi is about looking beyond the CDCL monoculture, using BDD based approaches as example.
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.
Published a rust crate to efficiently parse and write DIMACS CNF: https://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.)
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)
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 https://fgiesen.wordpress.com/2016/01/02/end-of-buffer-checks-in-decompressors/)
const BONUS_DATA_LEN: usize = 64;
The new placement of the http://docs.rs link for crates on http://crates.io trips me up... but since I learned how to write user scripts recently, I wrote one that adds a hotkey for it: https://gist.github.com/jix/f0cb842d4f321fbf5e8364160087f416
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:
A four part tutorial on proof complexity and how it relates to SAT solver performance by Sam Buss
https://youtu.be/_1ReDxKaJY8 (Part A)
https://youtu.be/hH9GLAFv3mk (Part B)
https://youtu.be/mNC45drVgPs (Part C)
https://youtu.be/ixgatFjc2GY (Part D)
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)
An introduction to approximate counting and sampling of solutions to SAT instances by Kuldeep S. Meel (@ksmeel@twitter.com)
Also a second talk with more details (it's a self-contained talk so there is some overlap)
A 4 part tutorial on solving and optimizing with Pseudo-Boolean constraints (linear constraints over Boolean variables) by Jakob Nordström
https://youtu.be/f8d9VxONa0E (Part 1)
https://youtu.be/aihmjopvuZQ (Part 2)
https://youtu.be/6VW1fsTYZcg (Part 3)
https://youtu.be/1_nd_Di4Vts (Part 4)
Currently there are a lot of great talks about SAT solving and related topics appearing on the Simons Institute youtube channel: https://www.youtube.com/c/SimonsInstitute/videos
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.
I often copy links from twitter, so I'm quite annoyed by https://t.co URLs. Finally wrote a simple userscript to resolve them so I can just right click to copy them: https://gist.github.com/jix/e67c127820954e1d1571c1f6f800ac2c
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
A while ago I wrote a small hacky script to auto run `cargo doc` on #rustlang source changes and to also serve the resulting docs locally using livereload so I don't need to refresh open browser tabs: https://gist.github.com/jix/caf2d46cebecb12d25eea27878bfceac
Maybe I'm not the only one who finds this helpful :)
The new vscode "wrap tabs" option (https://code.visualstudio.com/updates/v1_53#_wrap-tabs) 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 ^^
- Website
- https://jix.one
- https://twitter.com/jix_
Joined Aug 2020
