Jannis Harder

@jix_

Working on SAT solving with Rust. Spent a lot of time not finding better sorting networks. Not too bad at Tetris. he/him or they/them

Vrijeme pridruživanja: travanj 2009.

Tweetovi

Blokirali ste korisnika/cu @jix_

Jeste li sigurni da želite vidjeti te tweetove? Time nećete deblokirati korisnika/cu @jix_

  1. Prikvačeni tweet
    7. pro 2019.

    I'm super excited to announce a new result: sorting 11 inputs using a sorting network requires 35 comparisons and sorting 12 inputs requires 39 comparisons. I used a new search procedure w/ a formally verified checker, all on github: 1/11

    Prikaži ovu nit
    Poništi
  2. 22. sij

    It caught my eye, as I really like Lakatos' "Proofs and Refutations" about how proofs and definitions change and get patched when counterexamples are discovered or views shift and how that is part of mathematical progress. All using Euler's Poly. F. as ex.

    Prikaži ovu nit
    Poništi
  3. 22. sij

    I love reading books about the historical development of various mathematical subjects. I really enjoyed and just finished reading Richeson's "Euler's Gem" which covers the birth of topology, starting from Euler's polyhedra formula (+ history of that).

    Prikaži ovu nit
    Poništi
  4. proslijedio/la je Tweet
    16. sij

    If you are looking to hire "truly exeptional engineers and product persons" (quote of an external contractor) with a strong math background, or want to hire me, let me know. Team and I suddenly find us in the weird position of having to find new work. We are free starting... now!

    Poništi
  5. proslijedio/la je Tweet
    7. sij
    Prikaži ovu nit
    Poništi
  6. 25. pro 2019.
    Prikaži ovu nit
    Poništi
  7. 25. pro 2019.

    On my way back to Leipzig for the , looking forward to seeing lots of awesome folks again :) Also if we haven't met and you want to change that, feel free to say hi!

    Prikaži ovu nit
    Poništi
  8. 19. pro 2019.

    The core idea is to start with the semantics of a programming language and using types to encode facts about programs instead of starting with a formal system. Now I really want to write my own toy language/proof assistant based on that but my overflowing pile of projects says no

    Prikaži ovu nit
    Poništi
  9. 19. pro 2019.

    Somewhat unexpectedly youtube recommended a great lecture by robert harper about computational type theory: It's a different approach (vs formal type theory) that I haven't seen before and that makes some things less confusing.

    Prikaži ovu nit
    Poništi
  10. 15. pro 2019.

    A (German) talk on SAT solving I recently held is online now. Wish I had found more time to rehearse it, felt like a bumpy ride to me, but I got positive feedback anyway :)

    Poništi
  11. 7. pro 2019.

    The bound for 12 inputs follows directly due to an old result of Van Voorhis. Next I need to write up how and why all of this works. 11/11

    Prikaži ovu nit
    Poništi
  12. 7. pro 2019.

    Still it reduces the amount of work required from the verified part a lot, so I could use naive, easy to verify code and data structures. Today I finally got to the point where my formally verified checker printed `Just (11,35)` :) 10/11

    Prikaži ovu nit
    Poništi
  13. 7. pro 2019.

    Instead of directly checking the output of the search, I also introduced a post-processing stage that simplifies the output of the search and reduces it from ~100GB to ~3GB in size. Doing this during the search didn't work out. 9/11

    Prikaži ovu nit
    Poništi
  14. 7. pro 2019.

    The classic workaround here is to generate a certificate from the search and write a separate formally verified program to check that, in the hope that it'll be less work. That's also what I did. 8/11

    Prikaži ovu nit
    Poništi
  15. 7. pro 2019.

    To make sure my results were correct I wanted to formally verify my code. For formally verified code you usually have a performance/verification-effort trade-off. Compromising on the performance of the search wasn't an option though. 7/11

    Prikaži ovu nit
    Poništi
  16. 7. pro 2019.

    Scaling this to 11 inputs was still a challenge. Storing the explored search graph, would take over 1TB of memory. By recomputing the edges on the fly I managed to get this down to ~200GB. Making use of multiple cores was also tricky. 6/11

    Prikaži ovu nit
    Poništi
  17. 7. pro 2019.

    While working on this, I came up with an idea that allows to prune even larger parts of the search space and do so with less computation. With this I can get the bounds for 9 and 10 inputs in 10 seconds on my laptop. 5/11

    Prikaži ovu nit
    Poništi
  18. 7. pro 2019.

    Earlier this year I optimized that approach and got down to 2h on a 16-core machine ​. Experimenting with this made me realize that scaling this to 11 inputs would take way too much resources. 4/11

    Prikaži ovu nit
    Poništi
  19. 7. pro 2019.

    Finding the bounds for 9 and 10 inputs in 2014 took over a week on a 144 core cluster. In the meantime the approach used for that result was optimized to take 11h on a 32-core machine 3/11

    Prikaži ovu nit
    Poništi
  20. 7. pro 2019.

    These new lower bounds match the existing upper bounds, so we get two new terms of ​. The previous two terms were found in 2014 ​. The terms before that in 1966 by Floyd and Knuth. 2/11

    Prikaži ovu nit
    Poništi

Čini se da učitavanje traje već neko vrijeme.

Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.

    Možda bi vam se svidjelo i ovo:

    ·