Some context: I was thinking about the feasibility of using SAT solvers to prove primality, especially of Mersenne primes, by showing that there exists no Boolean sequence $d_1,d_2, ..., d_{b'}$ that can represent a divisor of the prime (i.e. UNSAT).

Given a Boolean list $d_1,d_2, ..., d_{b'}$, where $d$ is the base-2 representation of a base-10 positive integers $D$, does there exist a Boolean predicate that evaluates to True if and only if $2^b-1 \equiv 0 ($mod D)$?

(Assume $1 < D < N$, and hence, $b' < b$. Also assume $b$ is prime.)

Any help is greatly appreciated.

  • $\begingroup$ Isn't it just the case that any boolean-valued function of $b+b'$ boolean variables can be represented using Boolean algebra operations? $\endgroup$ – Daniel Schepler Feb 13 at 0:46

You could use a circuit which performs a modular reduction as explained in this lecture note (chapter 2.6.4 on page 32). The modular reduction computes the remainder of the division $N/D$. Use a digital comparator circuit to check for zero remainder. When the remainder vanishes to zero, the predicate becomes true.

From the cited lecture note: enter image description here

Note that this might not fully answer your question as it assumes $D$ to be a constant rather than a variable.

  • $\begingroup$ Close. However, can this be directly evaluated with Boolean logic? I want to implement the predicate directly (i.e. a sequence of logical operations). This is an interesting idea, though. $\endgroup$ – Baaing Cow Feb 12 at 22:52
  • $\begingroup$ Yes. An alternative would be to calculate the remainder $R$ as $R = N - D * (N/D)$. But that would require a divider, a subtractor and a multiplier. $\endgroup$ – Axel Kemper Feb 12 at 22:55
  • $\begingroup$ Subtraction and multiplication of Boolean arrays can be done as if it was in base-2. (subtraction is trivial XOR and NAND for carrying, multiplication can be expanded into addition, i.e. XOR and AND) This question concerns division. $\endgroup$ – Baaing Cow Feb 12 at 23:12
  • $\begingroup$ Divider circuits are actually described in the above-mentioned book Basic Arithmetic Circuits. My point ist that modular reduction is less complex than the classic remainder calculation. $\endgroup$ – Axel Kemper Feb 13 at 7:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.