axionbuster axionbuster

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

Introduction

Markov Jr. is an open source C# application that creates procedural content primarily via applying Markov rewrite rules to a 2D or 3D grid. A rewrite rule has an input and output pattern, which essentially specifies what pattern to look for in the existing grid, and what to replace it with.

For example, given a 2D grid, this would replace any white dot with a white cross:

***/*W*/*** :: *W*/WWW/*W*

The left hand side is the rule input, and the right hand side is the output. The / character is used to delimit rows, and space is used to delimit Z-layers (in 3D grids). The input rule above translates to the 2D pattern:

Some sample chunk data packets.

Format

The *.bin files are complete chunk data packet payloads (however, they do not have a packet length or ID specified, and are neither compressed nor encrypted).

The *.data.bin files are the data arrays within the packets, matching the data structure.

Most of these chunks have data only located in the bottom section, with a few exceptions. All of them have only the void biome set, and no block entities. The dimension is the overworld (skylight is present). All data is based on the format in 1.13.2.

	import Control.Monad (ap, forM_)
	import qualified Data.Map as M

	-- The Collapse Monad
	-- ------------------
	-- The Collapse Monad allows collapsing a value with labelled superpositions
	-- into a flat list of superposition-free values. It is like the List Monad,
	-- except that, instead of always doing a cartesian product, it will perform
	-- pairwise merges of distant parts of your program that are "entangled"
	-- under the same label. Examples:

	import Data.List (unfoldr, partition)
	import Data.Maybe (catMaybes)
	import Criterion.Main (defaultMain, env, bgroup, bench, nf)
	import System.Random (randomIO)
	import Control.Monad (replicateM)

	groupOn :: Eq k => (a -> k) -> [a] -> [(k, [a])]
	groupOn k = unfoldr f . map (\x -> (k x, x))
	where
	f [] = Nothing

	import qualified Data.Set as S
	import Data.Set (Set)
	import Data.Char (isLower)
	import Data.Ord (comparing, Down (Down))
	import Data.List (sortBy, subsequences, minimumBy, maximumBy)
	import Control.Monad.Trans.Writer.CPS
	import Data.Monoid
	import Data.Foldable (traverse_)

	wordFilter :: String -> Bool

	// helper functions

	// cnf formula exactly one of the variables in the chosen list to be true

	function ext_one(list) {
	let temp = ""
	temp=temp+atl_one(list)
	temp=temp+atm_one(list)
	return temp
	}

	-- how to model threaded comments (e.g. reddit comments) in SQL with a simple 'ancestors' column

	-- The comment tree:
	-- [1]
	-- / \
	-- [2] [4]
	-- / \ \
	-- [3] [7] [6]
	-- /
	-- [5]

	(* Code extracted from:
	SAT-MICRO: petit mais costaud !
	by Sylvain Conchon, Johannes Kanig, Stéphane Lescuyer
	*)

	module type VARIABLES = sig
	type t
	val compare : t -> t -> int
	end

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE DeriveFunctor #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE TypeOperators #-}

	module Indexed where

	-- Natural transformation..