Boolean Satisifiability Based ASIC Resistant Proof of Work¶

Matthew Wampler-Doty

Abstract: A “Proof of Work” (abbreviated PoW) system for a cryptocurrency based on providing logical formulae and variable assignments is proposed. Miners are required to both mine the logical formulae as well as provide variable assignments, as per the Stephen Cook’s celebrated Satisfaction Problem (abbreviated SAT) from his paper "The Complexity of Theorem Proving Procedures" (1970). To ensure the problem is non-trivial, formulae must conform to a large number of constraints, among them are: (1) they must have a fixed number of literals in each clause, (2) the graph of clauses must be connected, and a spanning tree traversal must be provided to prove this, (3) a minimal number of variables is necessary and finally (4) there must be exactly $N$ clauses. A naïve miner is proposed, and it is shown that it follows the same statistical behavior as the conventional BitCoin mining system. Given the nature of the problems this system is based on, we anticipate occasional algorithmic breakthroughs will result in speedups which will be difficult to introduce into ASICs, given their long development cycle. Verification is linear in the number of clauses in the mined solution.

Introduction¶

One of the problems facing Bitcoin is the rise of ASIC hardware specially designed for mining. These systems are designed to solve problems of the the form:

$$sha256(sha256(block\_header + nonce)) < target$$

Where $nonce$ is a free variable which may be incremented from some minimal value. Solutions to such problems constitute Proof of Work that is used as the basis for BitCoin. Since $sha256$ is straightforward to implement, ASICs can readily compute it in very few clock cycles, as compared to conventional CPU based architectures. As of November 2014, it is no longer feasible to mine BitCoin using a conventional CPU based architecture.

Alternatives systems are currently being investigated in the crypto-currency community to avoid this issue. One proposal is Hashimoto by Thaddeus Dryja (2014), who suggests using a two stage hash function. Another system, due to Vitalik Buterin, uses randomly generated logic circuits.

An independent thread of research involves mining protocols is based on traditional, Nondeterministic Polynomial (NP) problems from the mathematics literature. One such system is PrimeCoin, which is based on finding numbers that pass the popular test for primality using Fermat's Little Theorem. This was done to allow for reasonable control of inflation. As such numbers used in its blockchain are only probabilistic primes rather than true prmes, and some are not primes at all but rather composites known as Carmichael numbers (see A002997 in the Online Encyclopedia of Integer Sequences). A similar cryptocurrency, RieCoin, is also based finding prime numbers, but it uses the Miller-Rabin test to ensure true primality.

Traditional NP problems from computer science theory present an intriguing possibility for avoiding ASIC block chain mining. For algorithmically rich problems, speedups can come from researcher insight, rather than simple hardware improvements. Since ASICs have a long development cycle, this allows for savvy researchers to compete with ASICs designers and allow for CPUs to remain a competitive means of mining. In Boolean Satisfaction (SAT) in particular, researchers routinely report increases in performance in orders of magnitude (see, for instance, Duraira (2004), Aloul (2006), Velev (2009), etc.). It is noteworthy that all commercial SAT solvers are CPU based.

To this end, we propose SATCoin, for use as a Proof of Work specification based on SAT problems intended to be difficult to implement in an ASIC. We first go over how proof of work is verified, and then go on to present an algorithm suitable for mining.

Verification¶

In this section, we present the verification scheme for SATCoin, which exhibits linear time complexity.

Satisfaction¶

A satisfaction problem is the problem of finding an assignment of logical variables to either True or False such that a logical formula witha particular form is true. Formulae for SAT problems are presented in Conjunctive Normal Form (CNF), which are comprised of conjuncts of disjuncts of literals. A literal is a logical formula or its negation. Here is an example of a CNF formula:

$(A\vee \neg B \vee \neg D) \wedge \\ (\neg B \vee C \vee \neg D \vee E) \wedge \\ (C \vee \neg C \vee \neg A)$

SAT problems are solved by some assignment $\alpha$ of variables to either $True$ or $False$ that make each disjunct of the conjunct true. For instance, as long as $B$ is assigned to $False$, $E$ is assigned to $True$, and $C$ is assigned to $False$, all of the disjuncts of the above formula are made true.

In python, a literal can be modeled as an (immutable) object with two attributes: sign and a variable. A sign is either True or False, while variable is the name of the underlying variable.

A CNF formula can then be modeled as a collection of collections of literals. Here is how we'd express the example above:

An assignment can be modeled as a dictionary, with the keys being the variable names and the values being True or False.

Checking if a SAT problem is satisfied by a variable assignment is straight forward. We make the assumption that if a variable's truth value is not specified then it is False.

We can verify satisfied is implemented correctly by checking that our example evaluates to True:

SAT Problem Generation¶

We next a present how SAT problems are generated. We opt to allow SAT problems to be generated non-deterministically, allowing for the miner to construct the problem themselves.

To begin, define a linear congruential random number generator based on the secp256k1 elliptic curve that is used in BitCoin.

Next, we define the initial conditions for blockchain generation. A header is provided by the cryptocurrency network, which is a sha256 hash of the current blockchain. At the beginning of generation SAT problem generation, the miner selects a set of generators, which are all positive integers.

At each stage of SAT problem generation, the generators initially chosen are used to compute $n$ literals, using the latest random number $n$ supplied by next. For the $i$th generator $g_i$, the variable for its literal is $n \text{ mod } g_i$ while the sign is True if the $i$th lowest bit of $n$ is 1, and False if the $i$th lowest bit is 0. This is implemented as follows:

The miner then picks some number of literals from the generated literals to form a clause. The chosen generators are added to the current random value, and next is called on the result.

To give an example, suppose that the current random value is 3681122926843, and the user chose [9,13,14,21,33,35] as their initial generators. Then they could choose from among the following possibilities of literals to generate a clause:

Suppose the miner wanted to make a clause with 3 literals. Given the 6 possible generators, they would have ${6 \choose 3} = 20$ possibilities to choose from. Let's suppose they chose the literals generated by [9,21,33], then the next random value would be:

Putting everything together, we can verify if a miner correctly generated a SAT problem with the following check:

Here is an example with 8 generators:

Constraints¶

So far, we have presented SAT problems, and shown how a miner can non-deterministically construct one. Right now the problem has no constraints, however. In order to make the problem non-trivial, we introduce a series of structural constraints.

Constraints on Clauses¶

Fixed Number of Clauses¶

One simple criterion is to have a fixed number of clauses. More clauses put more constraints on the possible SAT solutions.

Clause Width¶

The first demand we make is that there be a specified number of unique variables in a clause; this is the clause's width.

Since it will come up somewhat often, here is a simple function for extracting the set of variables from a clause:

We can easily check that there are $n$ variables in a clause by checking the length of the result of clause_variables:

Unique Clauses¶

SAT problems with repitious clauses are easier to solve, so we will want to constrain problems so that no two have the same variables.

Here's an example of a set of clauses where everything is unique:

Here's an example with repeated clauses that we do not want to permit:

Connectedness¶

Another property we wish to enforce is that the graph of clauses must be connected. This enforces a certain level of interaction among all of the clauses; setting one literal can potentially force the value of any other literal.

To ensure that the graph of clauses is connected, we make use of the following observation:

Fact. A graph is connected if and only if there is a traversal of a spanning tree that visits every node.

Checking that a given traversal of a spanning tree visits every node can be carried out in linear time. To start, we define a binary predicate which asserts whether two clauses are connected:

A spanning tree traversal is represented as a list of data structures, each with two fields:

• An index of a clause in the SAT problem (the 'child clause index')
• An index of a parent clause in the SAT problem (the 'parent clause index')

In the case of the root, there is no parent clause, but all subsequent entries must have a parent clause. Morever, the parent clause must always have been a clause that's been previously listed, and the parent and child must be connected according to the connected predicate.

Given that the spanning tree traversal never repeats and has as many entries as clauses, we know that the graph of clauses is indeed connected.

It's of course helpful to see an example:

The resulting spanning tree can of course be easily recovered from the traversal. Here's the spanning tree used in the above example:

Constraints on Generators¶

Fixed Number of Generators¶

Similar to clauses, we also demand that there be a fixed number of generators:

Minimal Value For Generators¶

Some criteria for clauses are easy to satisfy with a choice of small generators. So we constrain the problem by presenting a minimal value for generator.

BitCoin Style SHA256 Checking¶

So far, we've presented a number of criteria for enforcing that the SAT problems generated by miners be non-trivial. Ideally, we'd like to be able to set a hard statistical probability that a proposed solution will pass.

We adopt the approach taken by BitCoin, but with a modification. We introduce the criterion that:

$sha256(block\_header,variable\_assignment) < target$

Like BitCoin, this effectively means that with probability $p$ a solution will be rejected, where $p = \frac{target}{2^{256}}$. Unlike BitCoin, where solutions can be found via linear search (simply incrementing a nonce value), the miner must instead enumerate possible satisifying variable assignments for a SAT problem they have constructed. Enumerating every satisfying variable assignment for a given SAT problem is #P-complete, which is NP-Hard. Of course, a miner could also try to compose other SAT problems with varying solutions, which is in NP.

Below we give an implementation of this criterion; we make use of the JSON representation of the variable assignment, although there are many possible representations.

Here is an example; as we can see, variable_assignment and block_header will pass if we are rejecting approximately $66.\overline{6}\%$ of solutions.

If we instead demand that approximately $75\%$ of solutions be rejected, this example does not pass.

Full Solution Validation¶

We now present all of our criteria together as a comprehensive proof of work validation scheme.

Mining¶

In this section, we present a mining algorithm. Since the acceptance criteria are open ended, there are many possible mining algorithms.

Mining, like ordinary SAT solving, can be carried out via heuristic backtrack search. Below is a simple depth first search algorithm making use of python generators. By construction, this algorithm runs in $O(EXP(n))$, where $n$ is the number of clauses.

Our solution makes use of a search state data structure; for simplicity we model it as immutable and copy-on-write. At each stage of the search, a pool of possible state transitions is lazily generated, and each one is searched recursively.

Below, we give how initial states are generated. Book keeping variables include: which clauses have been visited, the state of the constructed spanning tree, and the state of the variable assignment under construction.

Finally, we give how states are updated when new information arrives.

Putting it together, we can verify that indeed our mining algorithm satisfies our proof of work validation scheme

Performance¶

In this section, we look at the performance of the mining algorithm under different difficulties. A model for expected performance given a set difficulty is provided. We first show empirically that BitCoin mining conforms to this model, and then go on to show that SATcoin mining also conforms.

For Reference: BitCoin Mining Performance¶

In this section, we give a simple reference model for BitCoin mining: bitcoin mining time follows a geometric distribution with respect to difficulty.

We begin by assuming that sha256 is an unbiased, uniformly random value. For a set value, the probability that a given nonce will fail to return a hash with value less than $2^{256} / D$ is $1 / D$. This means that the number of times $X$ the miner must compute a sha256 hash to mine a currency is governed by a geometric random distribution:

$$\mathbb{P}[X = k] = \left(1 - \frac{1}{D}\right)^k \frac{1}{D}$$

Next, we model computing the sha256 hash of a block header and nonce, as in conventional BitCoin mining, as taking constant time $\hat{C}$. We can think of $\hat{C}$ as the time it takes to mine when difficulty is set to 0. Let $T$ be a random variable describing the time to mine a coin. We can derive a closed form for the expected time mine a bitcoin as follows:

$$\begin{eqnarray*} \mathbb{E}[T] & = & \sum_{k=1}^\infty \left(1 - \frac{1}{D}\right)^k \frac{1}{D} k \hat{C} \\ & = & \hat{C} \sum_{k=1}^\infty k \left(1 - \frac{1}{D}\right)^k \frac{1}{D} \\ & = & \hat{C} \mathbb{E}[X]\\ & = & \hat{C} \frac{1}{1 / D}\\ & = & \hat{C} D \end{eqnarray*}$$

This model predicts that expect time for mining should increase linearly with difficulty $D$.

We can test this model by writing a simple miner, as follows:

Timing for mining can be carried out using the standard python benchmarking library timeit:

We can now carry out Monty-Carlo experiments involving our expected time to mine model. Since our hypothesis is that mining should increase linearly with difficulty, it should fit nicely with a linear regression:

We can see that mining occasionally has some outliers which create spikes in the average mining time. This is a consequence of the geometric distribution; while the average time increases linearly with difficulty, variance increases quadratically. We can derive a closed form the variance as follows:

$$\begin{eqnarray*} \operatorname{Var}[T] & = & \mathbb{E}[T^2] - (\mathbb{E}[T])^2 \\ & = & \sum_{k=1}^\infty \left(1 - \frac{1}{D}\right)^k \frac{1}{D} (k \hat{C})^2 - (\hat{C} D)^2 \\ & = & \hat{C}^2 \operatorname{Var}[X]\\ & = & \hat{C}^2 \frac{1 - (1/D)}{(1/D)^2}\\ & = & \hat{C}^2 (D^2 - D) \end{eqnarray*}$$

Empirically, we should expect variance to roughly follow a quadratic formula $k + C_1 D + C_2 D^2$, which takes into account computational overhead and other sources of noise. This model should follow the idealized model closely; we expect:

1. $C_1 \approx - \hat{C}^2$
2. $C_2 \approx \hat{C}^2$

As we can see, our model's predictions are quite accurate for the projected variance of mining times.

Finally, we can infer a Cummulative Distribution Function (CDF) for mining time based on the geometric distribution; it is approximated as follows:

$$\mathbb{P}[T < x] \approx 1 - (1 - 1/D)^{x / \hat{C}}$$

Based on the CDF, we can perform hypothesis testing based on the Kolmogorov-Smirnov Test. The default in scipy.stats is two-sided.

Recall that the null-hypothesis in the KS-Test is that the two distributions are the same, and that we reject the null hypothesis when the p-value is high or the KS-Statistic is high. As we can see, the KS-Statistic itself is always low, while the p-value it typically low up to higher difficulties D. As D increases the underlying geometric distribution approaches an exponential distribution, where statistics can be dominated by outliar behavior even in Monty-Carlo experiments (a point Nassim Taleb makes at length in his writings, most notably The Black Swan (2007)).

SATCoin Mining Performance¶

Unlike bitcoin, the SATCoin protocol outlined has more difficulty parameters. The parameters we investigate are:

• Target Difficulty (same as BitCoin)
• Number of Clauses
• Minimal Generator

Target Difficulty¶

We begin by looking at adjusting the target difficulty. We observe that SATCoin follows the same geometric distribution statistics that BitCoin follows:

The statistical behavior of mining is the same as BitCoin, however there is a lot more variance and computational overhead. As we can see the average mining time increases linearly:

Similarly variance increases quadratically, however we can see that it is much higher than BitCoin:

As a result, our statistical hypothesis testing is also weaker:

This poor behavior may just be an artifact that our sample miner is written in Python rather than in C. However, below we see some other statistics that lead us to believe that our miner is in general less statistically stable than BitCoin mining.

Number of Clauses¶

Our miner, like all SAT solvers, performs backtrack tree search. We can thus expect that its worst case performance is exponential in the clause length. Since we are giving it random input, Murphy's law dictates we should expect it to stick to its worst case performance, especially because it is written quite naïvely.

Variance too scales exponentially with clause length:

While our miner is naïve, we have clearly defined mining as a kind of exponential search. As a consequence, we can expect that using the number of clauses as a measure of difficulty for SATCoin will lead to greater variance in coin issuance than BitCoin. On the other hand, dynamic clause depth is where SAT research shines the most, since theoretical breakthroughs such as conflict clause learning are arguably what have enabled advances in SAT over the last 10 years.

Minimal Generator¶

We finally look at restrictions on the minimal generator as a difficulty measure. Monty Carlo statistics once again suggests an exponential distribution.