Conditional on Conflux learning a "nice number", will a SAT solver find it relatively quickly?
12
95
571
resolved Apr 1
Resolved
N/A

@Conflux posted a market about whether they would find a "nice number" above 69. This market gives a high-level sketch of a particular algorithm for potentially finding new nice numbers.

If the above market resolves "YES", then I will code the algorithm in Python and run it on my 2021 MacBook Pro. If the program finds a nice number with the given base within 3 hours then this resolves YES, otherwise NO. If the linked market isn't resolved, or if we don't know the base of the number, this resolves N/A.

The algorithm will work like this: I will encode the "niceness checking" algorithm as a boolean circuit as follows.

  1. I will encode the nice number as an input to the circuit as a single binary longer big enough to represent any number within the "range" for the base b (see the description of the range in the blog post).

  2. I will compute the square of the number as a binary number by multiplying it by itself using naive multiplication.

  3. I will compute the cube of the number by multiplying the number by its square, again using naive multiplication.

  4. I will compute the digits of the square and the cube in the base b (represented as lists of log2-of-b bit numbers of size) by iterative division and remainder by b.

  5. I will do a pairwise comparison of each of the digits of the square and cube to ensure they are distinct.

I will then use a SAT solver from the PySAT suite to attempt to solve this circuit for an input that satisfies the condition.


Close date updated to 2023-03-31 3:59 pm

Get Ṁ200 play money
Sort by:
bought Ṁ400 of NO

The reason I bid this down is it doesn’t make sense for me that this market would be above linked market.

Here’s why: if you believe that if given a base with a nice number, the nice number can be found in three hours or less with a SAT solver, then you should code this up and check the bases 40–150, spending three hours on each before terminating the search. This would take “only” ~13.75 days of computing.

predicted NO

@JoshuaB But if no such number exists, this market resolves N/A (YES bettors get their money back) and the other resolves NO (they lose it). If you think there's a 95% chance that there's no such number, 4% there is and it's hard to find, and 1% it's easy, you should bid this market to 20% and the other to 5%.

sold Ṁ88 of NO

@jfjurchen Aha, yes, conditional probability. I don’t know why, despite “conditional” being in the title, my brain completely skipped over conditional probability being useful. Thanks for pointing this out!

bought Ṁ20 of NO

If any examples are found (which is unlikely), they almost certainly won't be found by brute force. We already know that examples don't exist for small bases, and the estimated probability of a number within range being a nice number in base b is b!/b^b, which gets very small as b increases. For the bases large enough that nice numbers are actually expected to exist, the probability is so small that finding an example would probably be impossible to do in any reasonable amount of time (let alone 3 hours) no matter how powerful your computer is.

bought Ṁ10 of NO

Implemented some examples in Z3Py because it seemed easier than PySAT (though it does SMT instead of SAT!).
For the problem where x and x² must contain all digits, my code found examples in these times:

Base 6: 0.14 seconds

Base 8: 0.58 seconds

Base 9: 182 seconds

And a similar script found the 69 example in base 10 in 76.5 seconds.

Does anyone know if PySAT tends to be much faster than Z3Py?

bought Ṁ60 of NO

I’m interested to see this working, so I’ve added, uh, Ṁ321 as subsidies into the market. Good luck!!

Also should the close date be March 31, 2023, like the linked market?

predicted YES

@JoshuaB Thanks!

You’re only gonna do this if someone else finds a nice number first?

bought Ṁ10 of NO

@Conflux I should also say, I think it’s an interesting approach!

predicted YES

@Conflux Well I was going to do it if people thought it was a workable approach. I’m sort of surprised people value this so low, maybe people think that if they buy NO that will provide profit incentive for me to do it anyway. The issue is that while I think would work for similar problems at smaller scale, doing it for a base around 120 seems big.

predicted NO

@BoltonBailey I’m mainly just skeptical that this cuts down enough on the orders of magnitude.

How fast is this for base 10?

predicted YES

@Conflux Feel free to implement yourself and find out (if you do I'd appreciate the code so I don't have to code it myself if the conditional market resolves YES)

predicted NO

@BoltonBailey I’ve never used pysat before, but maybe if I have some spare time!