All current mainstream ciphers are relatively easy to transform into SAT form. This is a proposal for a fallback for that, using polymorphic constraints between the bits via sboxes that are part of the private key.
Suggested changes to avoid redoing XChaCha20: since the sboxes could be the entire private key, what was the key could be a 256 bits nonce, and what was the nonce could be the counter, and what was the counter could be a stream index: such a modification could be called yadacha20.
Small, self-contained super ugly, quickly written Rust code: this is an initial draft of a work in progress. The goal of this post is to get feedback as early as possible.
Thank you.