2026-01-09 # Redstone with SAT solvers
toki lili TL;DR
An off-hand comment on Discord led from one rabbit-hole to another. In the end, I formalized
redstone (meaning dust, torches, and blocks) into CNF notation, so I could make SAT solvers create
redstone circuitry for me.
open Introduction:
Last week, someone asked a question about redstone in the Scicraft Discord server. They wanted to find a simple way to build a unary counter out of redstone. One of the follow-up responses posted a solution that used locking repeaters:
I found the post interesting, and offered a joke comment. In particular, I was curious if anyone could replicate the design out of redstone torches, dust, and solid blocks. Redstone dust and torches were the first parts of redstone to be added. At one point, these were the only logic building blocks available to players. Even so, they were sufficient for complicated logic.
lon ilo Creating Redstone:
As a challenge to myself, I tried to create redstone circuits with this restriction. As it turns out, redstone can be hard! I had also decided to build circuits that are one-block wide, so I could place them together more easily. After some trial and error, I made my first D-type flip-flop:
I was not very pleased with this design. As you can see, the design is large, and there’s not an easy way to access the output. After consecutive tweaks, I settled on a smaller design. When working at this level of redstone, you soon realize that the higher structures you took for granted (eg. a rising edge detector) need to be implemented literally.
(Redstone dust can be either "on" or "off". It supplies power to the blocks it is on top of, or
horizontally touching. It is connected to dust on the left and right, and can be connected in
diagonals as well, with some constraints. Redstone torches are inverters. They are "off" if
their supporting block is powered, otherwise they are "on". Torches power the block above them
("strong" powering, so redstone in contact with that block is also "on"), and also powers dust
to the side or directly below themselves.)
In the top left of this circuit you can see the rising edge circuit, then you can see the set and reset sections below and to the right, as well as the "memory" or latch for the circuit. This circuit can likely be optimized more. It is pretty fun to play around with, however. Due to the placement of the output line and input block, it is simple to set this up into a binary counter (game running at greater speed than normal):
ike Complications:
Over the past week, I got fairly obsessed with the concept of this "primitive" redstone. In the game of Minecraft, you can get access to redstone dust and torches far easier than most other components. If you play this game on a no-structure, super-flat world (an infinite plane of grass, without things like villages appearing), then you could build any of these redstone contraptions just with the blocks below your feet and the items that drop from killing Minecraft witches. As such, I thought it would be a fun idea to design a computer that can be built with these limitations, starting with a bidirectional redstone CPU bus:
The logic I was trying to form here needed to become more complex than latches and flip-flops, however. In attempting to build my first vertical full-adder, I ran into a roadblock. How do I possibly say that one signal crosses another, in a one-wide redstone circuit? As far as one redstone line or torch is concerned, this should be impossible. Well... I thought it would be impossible. As it turns out, there is actually a way to simulate two wires crossing, without wires actually crossing, using NAND gates:
So in reality, you could build anything you want in a one-wide space - and have it be Turing complete - in Minecraft, using only redstone dust, torches, and blocks. The only issue would be how tall and long this build is... Just the circuit shown here is already plenty large to encode in redstone. The complexity of optimizing a full-adder is not something that I wanted to attempt by hand. Enter the SAT solver.
ilo nanpa SAT Solvers
SAT solvers are programs that take a large equation with many booleans, and finds value for each boolean, such that the overall equation is true. With brute-force solving, you will find the solution to an equation with 32 variables after at most 2^32 (approximately 4 billion) steps. With each additional boolean, a brute-force solver will take twice as long to solve the problem.
SAT solvers are absolute beasts. I have previously used them to solve equations with tens of millions of variables and hundreds of millions of clauses. (If you are wondering, I was making the SAT solver find me optimal sets of self-synchronizing codes.) In short, they have a smart algorithm which recognizes patterns and shortcuts while attempting to solve the equation. (This is the base algorithm; solvers like "cadical," "kissat," and "glucose" have many more internal heuristics governing how this algorithm is run.)
Still not getting it? Imagine this: you are abysmal at division, but very good at multiplication and addition. If you have the numbers 23 and 84, and you want to know what 84 divided by 23 is, you can write the equation as "84 equals 23 times a quotient plus a remainder." Now, you write each number (and the unknown numbers) as 8-bit unsigned integers, and create boolean equations for a full-adder, textbook multiplier, etc. You tell the SAT solver that the bits for these variables belong to these equations. When you throw this problem at the SAT solver, the only result for the unknown variables that satisfy the multiplication and addition would be the same as dividing the number in the first place.
(It's quite fun to throw factorization problems at it this way too - although it's not as fast
as the general number field sieve (The SAT solver has to generate these constraints through the
solving process that GNFS already knows and exploits).)
To put it simply, I wanted to make my redstone builds smaller, so I decided to formalize the concept of redstone in a way that a SAT solver could understand it. This means that I had to tell the SAT solver that a torch would invert the power of the block supporting it, redstone dust would propagate signal strength to nearby redstone dust (except it would be one-less than the current power strength), etc.
SAT solvers commonly use something called conjunctive normal form (CNF) to encode this problem. The file format for how CNF is represented to SAT solvers starts with a header "cnf [variable count] [constraint count]", followed by one constraint per-line. Variables start at one, and increment for each consecutive variable. Each clause must be true for the problem to be solved. One clause could be "2 -4 8 9 0" - meaning that variable 2 is true, OR variable 4 is false, OR variable 8 is true, OR variable 9 is true. The "0" denotes the end of the clause.
It would be far too much for me to write the CNF by-hand. As such, I wrote a program in Zig to encode the problem (much is omitted):
// -------------------------------------------------------- CNF ENCODING GLOBALS
const gpa = std.heap.smp_allocator;
var cnf_content: Allocating = .init(gpa);
var cnf_constraint_count: u64 = 0;
var cnf_variable_count: u64 = 0;
// ------------------------------------------------------------- ALLOCATING BITS
fn alloc() u64 {
cnf_variable_count += 1;
return cnf_variable_count;
}
// -------------------------------------------------------- ENCODING CONSTRAINTS
/// serialize some number of CNF constraints to the constraints list
fn constrain(indexes: []const u64, identities: []const u1) !void {
const writer = &cnf_content.writer;
for (indexes, identities) |index, identity| switch (identity) {
1 => try writer.print("{} ", .{index}),
0 => try writer.print("-{} ", .{index}),
};
try writer.writeAll("0\n");
cnf_constraint_count += 1;
}
/// serialize bitblaster state
fn writeCnf(writer: *Writer) !void {
try writer.print("p cnf {} {}\n{s}", .{
cnf_variable_count,
cnf_constraint_count,
cnf_content.written(),
});
}
// --------------------------------------------------- DOUBLE BITWISE OPERATIONS
/// result <- lhs NOR rhs
fn bitnor(lhs: u64, rhs: u64, result: u64) !void {
try bitop2(lhs, rhs, result, .{ 1, 0, 0, 0 });
}
/// result <- lhs AND rhs
fn bitand(lhs: u64, rhs: u64, result: u64) !void {
try bitop2(lhs, rhs, result, .{ 0, 0, 0, 1 });
}
/// result <- lhs XOR rhs
fn bitxor(lhs: u64, rhs: u64, result: u64) !void {
try bitop2(lhs, rhs, result, .{ 0, 1, 1, 0 });
}
fn bitop2(a: u64, b: u64, c: u64, t: [4]u1) !void {
try constrain(&.{ a, b, c }, &.{ 1, 1, t[0] });
try constrain(&.{ a, b, c }, &.{ 1, 0, t[1] });
try constrain(&.{ a, b, c }, &.{ 0, 1, t[2] });
try constrain(&.{ a, b, c }, &.{ 0, 0, t[3] });
}
With the bare-bones code in place, I was free to write higher level constructs. For example, I know that redstone dust must be placed on top of a block, torches are on if and only if their supporting block is not powered, dust is powered if and only if it’s signal strength is not zero, blocks are strongly powered if above a torch, etc:
// Blocks are weakly powered if adjacent to a powered dust block
fn enforceWeakPowering() !void {
for (0..states) |state| {
for (0..width) |x| {
for (0..height) |y| {
const r = isDustPoweredOffset(state, x, 1, y, 0); // right ON
const l = isDustPoweredOffset(state, x, -1, y, 0); // left ON
const t = isDustPoweredOffset(state, x, 0, y, -1); // top ON
const p = is_weakly_powered[state][x][y]; // block is powered
const r_or_l = alloc();
try bitor(r, l, r_or_l);
const r_or_l_or_t = alloc();
try bitor(r_or_l, t, r_or_l_or_t);
try bitand(is_block[x][y], r_or_l_or_t, p);
}
}
}
}
ike nanpa wan Problem 1:
If you were paying careful attention to the last block of code, you may have noticed that I have some number of "states" I am encoding in parallel for this redstone circuit. The problem is, how does one encode the constraint that a redstone circuit equals the expected output for all provided inputs? My solution is to simulate different signal/power levels for each possible truth-table row. I tell the SAT solver that the blocks must be identical between each state, and the power level of each redstone dust can be distinct between each state (but I don’t specify where the blocks are, so it will set that up for me - they are the "undefined variables").
With the first problem solved (via the concept of "states") - we are able to formalize the logic of any truth table within a given area (specifying explicit inputs and output positions). And at last, we get an output from the SAT solver that *definitely* makes sense... Wait, why are the outputs not connected to the inputs?
ike nanpa tu Problem 2:
The output from my program isn’t the easiest to read - I wrote it in a half-hour to quickly display block types after parsing the output from a SAT solver. The left side has inputs, the right side has outputs... This *should* be finding a circuit that has the same truth table as an XOR gate. So why is nothing connected!?!? Well... according to the constraints it has, this *is* a valid XOR gate.
Do you remember when I said that we would fix problem one by making some number of identical copies of the redstone circuit, where only the power levels or "state" of the redstone would vary between each instance? You may have already guessed the problem - the SAT solver created memory in the form of a latch. On the top right of the image above, you will notice that four torches, four blocks, and two redstone dust form a latch. Because the power level of each component can be dif and only iferent for each row in the truth table we want, the SAT solver decided to encode the correct answer into this latch for each state.
The solution here is to write more CNF to prevent the SAT solver from creating any latches. How do we do this? As far as I am aware, the software that people use to simplify hardware circuits forces signals to propagate from left-to-right, to prevent any "loops." In a sense, we need to do the same thing here... But redstone dust is bidirectional. We can prevent redstone dust from being more than one block wide, or prevent signal strength of a redstone dust line from strictly decreasing right-to-left, but this would ruin the point of trying to get it to optimize builds for me.
So how do we do this? Well, my solution is to create the concept of an acyclic directed graph in the generated redstone. Here are the rules: When a "source" of power reaches a "sink," eg. a torch is next to a piece of dust, we say that some "ID" that the two individually have is strictly transitive - or one is less than the other, using code like this, for example:
// dust have lesser ID than the torch next to or above them
fn restrictDustTorchId() !void {
for (0..width) |x| {
for (0..height) |y| {
const id_current = segment_id[x][y];
const lt_id_left = alloc();
const id_left_block = segmentIdOffset(x, -1, y, 0);
try lessthan8(id_current, id_left_block, lt_id_left);
const check_left = alloc();
try bitand(isTorchOffset(x, -1, y, 0), is_dust[x][y], check_left);
try bitimp(check_left, lt_id_left);
const lt_id_right = alloc();
const id_right_block = segmentIdOffset(x, 1, y, 0);
try lessthan8(id_current, id_right_block, lt_id_right);
const check_right = alloc();
try bitand(isTorchOffset(x, 1, y, 0), is_dust[x][y], check_right);
try bitimp(check_right, lt_id_right);
const lt_id_above = alloc();
const id_above_block = segmentIdOffset(x, 0, y, -1);
try lessthan8(id_current, id_above_block, lt_id_above);
const check_above = alloc();
try bitand(isTorchOffset(x, 0, y, -1), is_dust[x][y], check_above);
try bitimp(check_above, lt_id_above);
}
}
}
/// 8 bit less-than based on overflow from subtraction
fn lessthan8(lhs: [8]u64, rhs: [8]u64, lt: u64) !void {
var borrow: [7]u64 = undefined;
for (&borrow) |*x| x.* = alloc();
try halfsub(lhs[0], rhs[0], alloc(), borrow[0]);
try fullsub(lhs[1], rhs[1], borrow[0], alloc(), borrow[1]);
try fullsub(lhs[2], rhs[2], borrow[1], alloc(), borrow[2]);
try fullsub(lhs[3], rhs[3], borrow[2], alloc(), borrow[3]);
try fullsub(lhs[4], rhs[4], borrow[3], alloc(), borrow[4]);
try fullsub(lhs[5], rhs[5], borrow[4], alloc(), borrow[5]);
try fullsub(lhs[6], rhs[6], borrow[5], alloc(), borrow[6]);
try fullsub(lhs[7], rhs[7], borrow[6], alloc(), lt);
}
/// bitwise half subtractor, a - b = s - o * 2
fn halfsub(a: u64, b: u64, s: u64, o: u64) !void {
try bitop2(a, b, s, .{ 0, 1, 1, 0 });
try bitop2(a, b, o, .{ 0, 1, 0, 0 });
}
/// bitwise full subtractor, a - b - i = s - o * 2
fn fullsub(a: u64, b: u64, i: u64, s: u64, o: u64) !void {
try bitop3(a, b, i, s, .{ 0, 1, 1, 0, 1, 0, 0, 1 });
try bitop3(a, b, i, o, .{ 0, 1, 1, 1, 0, 0, 0, 1 });
}
It should also be noted that the "bitimp" function introduces a logical (not mathematical) implication between two variables. In other words, If X implies Y, then Y is true IF X is true, otherwise, Y could be EITHER true or false. This is VERY IMPORTANT for the problem here - because you want to add constraints depending on other constraints, and a typical implication would enforce things we don’t want here.
pini Results
The finished program, while not easily configurable, is capable of creating SAT problems which (when satisfied) encode the position of different components for a redstone circuit. At the time of writing, I am running it to generate a one-wide redstone dust, torch, and block full-adder for me.
I would say that this project is a complete success - it found a very small XOR gate for me, the logic of which is contained within a 6 by 7 block area! This result is far smaller than my original attempt:
The output of the program for the above output includes some unnecessary logic, which I trimmed:
Thanks for reading :)