I wrote it by hand but I thought about Rossete. I’ve watched one presentation about Rossete (that is the max I know) and I remember the presenter saying that it is possible that satisfy a predicate and is optimized for size. I definitely need to check it out.

I have to catch up! Missed the last two days and I just finished day 21. I will work on 20 and then finish the second part of day 19.

By the way, is it possible to express any Boolean expression in springscript?

I think we can’t, but I might not be thinking correctly about the problem.

(not A and not B) or (not C and not D)

I don’t see how I could write a springscript (with only two writable registers) to express this expression.

Is there a way?

I just realized I probably should have posted stuff here to prevent spoiling people. Sorry about that.

@wanderley.guimaraes here’s a Rosette code to generate a springscript equivalent to (not A and not B) or (not C and not D)

And the springscript output from the above program is

OR C J OR A T OR D J OR B T AND J T NOT T J which uses 6 instructions. Note that when I tried 5 instructions Rosette says there’s no solution, so 6 is the shortest program.

We just synthesize De Morgan’s law, pretty much :slightly_smiling_face:

Can you express any propositional formula in springscript? Answer yes.

Proof: Any propositional formula can be converted to CNF. It is enough to use the temporary register for one CNF clause. Therefore, we can accumulate results from each clause into the output register.

Claim: It is enough to use the temporary register for one CNF clause

Proof: For a CNF clause (or A1 … An (not B1) … (not Bm)) , emit the instructions

NOT B1 T NOT T T which sets T to B1 .

Then, conjoin it with the rest of Bi , and then use De Morgan’s law to obtain (or (not B1) ... (not Bm)).

AND B2 T ... AND Bm T NOT T T And now disjoin it with the rest of Ai .

OR A1 T ... OR An T which gives us the desired result.

Thanks for the code example and the proof!

One thing to keep in mind is the the usual CNF conversion — Tseitin transformation — doesn’t work here

because Tseitin transformation doesn’t maintain logical equivalence. It only maintains equi-satisfiability.

So you need a much more expensive CNF conversion. The point of Tseitin transformation is that it can be done in polynomial (in fact linear) time, but converting to CNF while maintaining logical equivalence is not known to be possible in polynomial time. This is in fact equivalent to asking whether P =? NP