Conditional on Conflux learning a "nice number", will a SAT solver find it relatively quickly?
12
571Ṁ1520
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
Ṁ1,000
to start trading!
© Manifold Markets, Inc.TermsPrivacy