mateon1’s gists

mateon1 / _skeletcps.py

Last active December 25, 2022 15:32

Closed Position Set (CPS) TM decider

	from bbconv import *
	from collections import deque

	# Machine, N - segment length, s - initial state, p in [0..N) - initial position, t - tape state encoded as an integer
	# returns (p, t, s) - final position, tape state, head state
	def segrun(M, N, s, p, t, limit=-1):
	seen = set()
	while 0 <= p < N:
	#print(": " + bin(t)[2:].zfill(N)[::-1])
	#print("- " + " "*p + "^")

mateon1 / fasttm.py

Created September 11, 2022 01:40

Accelerated turing machine simulators in python utilizing memoization

	from bbconv import *

	# Machine, N - segment length, s - initial state, p in [0..N) - initial position, t - tape state encoded as an integer
	# returns (p, t) - final position and tape state
	# OR None if
	def segrun(M, N, s, p, t, limit=-1):
	seen = set()
	while 0 <= p < N:
	#print(": " + bin(t)[2:].zfill(N)[::-1])
	#print("- " + " "*p + "^")

mateon1 / region.py

Created September 1, 2022 19:10

MC Anvil region unpacking/packing script

	import sys, os, zlib, struct

	def decompress_chunk(chunk):
	l, = struct.unpack_from(">I", chunk, 0)
	assert l <= len(chunk)-4, "Invalid length"
	assert chunk[4:5] == b"\x02", "Only zlib-compressed chunks are supported"
	return zlib.decompress(chunk[5:4+l])

	def compress_chunk(nbt):
	chunk = b"\x02" + zlib.compress(nbt)

mateon1 / _fwdseg.py

Last active September 4, 2022 00:43

Forward segment TM decider

	from bbconv import *
	from collections import deque

	# Machine, N - segment length, s - initial state, p in [0..N) - initial position, t - tape state encoded as an integer
	# returns (p, t) - final position and tape state
	# OR None if machine loops
	def segrun(M, N, s, p, t, limit=999999999):
	seen = set()
	while 0 <= p < N:
	#print(": " + bin(t)[2:].zfill(N)[::-1])

mateon1 / 36909813-N17-hs-trace.txt

Created July 20, 2022 23:08

https://bbchallenge.org/36909813 - Halting Segment SAT implementation, halting trace for centered N=17 cell tape

mateon1 / 7410754-N17-hs-trace.txt

Created July 20, 2022 21:32

https://bbchallenge.org/7410754 - Halting Segment SAT implementation, halting trace for centered N=17 cell tape

mateon1 / 7410754-N15-hs-trace.txt

Created July 20, 2022 21:05

https://bbchallenge.org/7410754 - Halting Segment SAT implementation, halting trace for centered N=15 cell tape

mateon1 / bbconv.py

Created July 17, 2022 14:52

Convert bbchallenge seed database format into a more compact and computer friendly binary format

mateon1 / theory.chess.check30.init.py

Created June 23, 2022 20:31

Checkmate 30 kings, SAT constraints

	# Based on https://puzzling.stackexchange.com/questions/116750/checkmate-30-kings-with-rooks

	def varchar(lit, seen=None):
	if seen:
	return {(True, True): "X", (True, False): "#", (False, True): ".", (False, False): "?"}[(lit in seen, -lit in seen)]
	else:
	v = slv.val(lit)
	if v is True: return "#"
	if v is False: return "."
	assert v is None

mateon1 / theory.turing.init.py

Created June 23, 2022 16:58

SAT solver TM code

	def varchar(lit, seen=None):
	if seen:
	return {(True, True): "X", (True, False): "#", (False, True): ".", (False, False): "?"}[(lit in seen, -lit in seen)]
	else:
	v = slv.val(lit)
	if v is True: return "#"
	if v is False: return "."
	assert v is None
	if slv.resolvemerge(lit) != lit: return "/"
	if len(slv.lit_refs[lit]) + len(slv.lit_refs[-lit]) == 0 and len(slv.idag.b[slv.idag.base(lit)]) == 0 and len(slv.idag.b[slv.idag.base(-lit)]) == 0:

Mateusz Naściszewski mateon1