I'll be there

I'm not aware of any usable tools for the numeric methods. The one time I tried to DIY it following the literature, I eventually gave up, but that's also a bit out of my area so YMMV.

I've had some limited success with symbolic methods using SMT solvers like z3: microsoft.github.io/z3guide/docs...

There are numeric methods based on the "Positivstellensatz" and "sum-of-squares optimization" and symbolic methods based on "cylindrical algebraic decomposition" and integration of that into "satisfiability modulo theories". (Quoted terms have WP articles.)

The solution set for inequalities of polynomials is called a "semialgebraic set".

There are algorithms that can check whether a solution exists and that can find an optimal one, but compared to either just linear inequalities or just polynomial equations, they are really complex and inefficient.

That was a fun problem to work on, thanks for sharing the link.

I learned about the connection between well-quasi-orderings and regular languages, which seems to have done the trick for this problem, but also feels like something I might end up finding other applications for.

In all the CDCL SAT solvers I'm familiar with (including my own) assumptions for incremental solving are handled as forced top-level decisions, so there's no difference between backtracking and removing incremental assumptions. Are SMT internal SAT solvers using a different approach here?

Is dancing links from Knuth's exact cover algorithm cool enough? en.wikipedia.org/wiki/Dancing...

I think the watched literals technique used in SAT solving is even cooler, but it's not really a case of "undo on backtrack" (did you mean that with Boolean constraints being more subtle?)

In the summary they write the algorithm can recover the key for multiple pairs using the same key, but that's the first time they mention it and they follow it up by "Further research is warranted to explore this issue.".

I'm inclined to just try out how hard breaking this cipher is for SAT solvers

Also the way I interpret the example they give towards the end of that paper, they're not solving a hard problem at all since finding 5 roundkeys matching a single plaintext/ciphertext pair is an under-constrained problem and only requires attacking a single round.

www.sciopen.com/article/pdf/... is what I looked at. Not even sure they use any quadratic terms. What's also not clear to me is whether this performs better than using the same overall approach together with the usual approaches for solving CNF or MILP. I'm also not familiar with the attacked cipher

I've only skimmed the paper, but it looks like they start with a MILP encoding of the cipher, constructed similar to how you'd come up with a CNF encoding, and then convert that to the model supported by D-Wave. I think the objective corresponds to modelling part of the cipher as soft constraints.

In the paper I'm looking at, the target model allows for a quadratic objective, quadratic constraints and all variables are binary variables. Linear constraints together with binary variables is already a superset of CNF-SAT and can easily encoding any circuit SAT problem.

Yeah. There's also another equivalent variant that uses a special kind of existential quantifier with restricted dependencies on universal quantified variables and that's how DQBF is usually defined (e.g. in github.com/jurajsic/DQB...). After Skolemization that turns into what I described.

I really hope I didn't make a mistake while trying to fit it into the character limit. it's certainly not the most illustrative description of DQBF

did you run across DQBF as an example for a NEXPTIME-complete problem? It's my favorite. Take a prop. formula φ over vars X, Y, … and terms f(U, V, …), g(…), … where each term applies a different n-ary function to some of the vars and terms may occur repeatedly. Decide whether∃f, g, …, ∀X, Y, …, φ.

Linux has a dedicated `close_range` syscall for this use case: "[...] listing open file descriptors in /proc/self/fd/ and calling close(2) on each one. close_range() can take care of this without requiring /proc and within a single system call, which provides significant performance benefits."

cursed thought: cubical c++ with std::univalence

(en.wikipedia.org/wiki/Homotop... for context)

I don't know any go, but it seems the if and else branches here are the wrong way around: github.com/mattn/bsky/b...