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.
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:
Note that this might not fully answer your question as it assumes $D$ to be a constant rather than a variable.