Andrey Vlasov Mr-Andersen

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

How to use Idris 2 in devcontainer

Step 1: build executable and libraries

Use the Dockerfile below to build the Idris 2 executable and standard library:

docker build --tag=idris2 .

	-- list derivation
	-- data [a] = [] \| a : [a]
	{-
	l = 1 + a ⋅ l
	l - a ⋅ l = 1
	l (1 - a) = 1

	l = (1 - a)⁻¹

	∂l = -1 ⋅ -(1 - a)⁻²