600 On The 3Sat

Boolean satisfiability is a classic problem in computer science. Given a series of n boolean variables, A B C ... and a formula in 3-conjunctive normal form

((¬ A ∨ B ∨ C) ∧ (D ∨ ¬ C ∨ E) ...)

This clause would be read Both "not A or B or C" and "D or not C or E" The goal is to find values for A B C that makes the formula true. For example, in the toy example, if both B and D are true, any other assignment works for A, C, and E. The Cook-Levin theorem shows shows that this problem is so hard that an efficient general solution to this problem would solve a host of other "NP complete problems" Knowing how hard this problem is in general makes it even more shocking that there exist practical 3sat solvers that work on instances with 100s if not 1000s of variables.

Through focused diligent research, CDCL (clause driven conflict learning) methods are the state of the art methods for solving 3Sat, and it's truly marvelous, that humans even have a shot at understanding this problem. However, every once in a while there are armchair mathematicians that seem to believe, that they can do better. P = NP, and their 20 line algorithm proves it.

600 On the 3Sat is a facetious exploration of these less than theoretically motivated approaches, and an analysis of how wrong these approaches are compared to the state of the art clause driven conflict learning solver. (repo)

The code used to display the table is adapted and reproduced with an MIT License from this codepen

We tried a number of optimization strategies: For each value of n we ran a few repeats of each algorithm on a few different random instances of 3sat with n variables and 4.5 * n (chosen within the "critical region" for random 3Sat") clauses. Each clause consisted of 3 random variables with a .5 chance of negating any variable. The column marked with the strategies name was the average response of the strategy, 1 = Satisfiable, 0 = unsatisfiable, strategy_correct is the fraction of said responses that are correct, and strategy_time was the time it took to receive the answer. Strategies that operated too slowly, were cut off from future trials, so most of this chart has no data on it. Some of the results were shocking, some, not so much. We first, have an empirical proof that P != NP, so I accept wire transfers, or mailed checks for the millenium prize. In Lieu of cash, I accept proofs of other millenium prize problems \s. But, what's really intereesting is that open source integer linear programming methods, are indeed outperformed by specialized SAT solvers. Specialized methods could solve problems of size n < 100 in less than 1 / 20 seconds. While, ILP started timing out well before that. Schonig's algorithm appeared to outperform any hand-rolled algorithm, including the "improvement" suggested by the arxiv paper, my own manual gradient descent type approach to SAT, black box hyperparameter tuning methods, and black box function optimization from scipy. Even worse, is that for problem sizes that any of these in-house methods were able to solve, simply brute forcing the O(2^n) inputs was faster. The lessons here are three-fold: don't reinvent the wheel. There is no "strong evidence" for the correctness of an algorithm without either a certified peer reviewed proof, or a real implemetation of the algorithm. Lastly, if you do feel the need to reinvent the wheel. Don't get too creative.

Time as a function of number of variables for each strategy until time out was reached.

Fraction of instances solved by each method

CDCL is a complete and sound method, so the canonical solver line is also the number of solvable instances.



Source
        
import random
import pandas as pd
import collections
import time
import pysmt
from pysmt.shortcuts import Symbol, LE, GE, Int, And, Equals, Plus, Solver, Or, Iff, Bool, get_model
from pysmt.typing import INT
from mip import *
from functools import reduce
from itertools import combinations
from operator import mul
from scipy.optimize import minimize
from hyperopt import fmin, tpe, space_eval, hp

critical_ratio = 4.4
REPEATS = 10
TIMEOUT = 20
MIN_N = 3
MAX_N = 1000

# https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/RND3SAT/descr.html#:~:text=One%20particularly%20interesting%20property%20of%20uniform%20Random-3-SAT%20is,systematically%20increasing%20%28or%20decreasing%29%20the%20number%20of%20kclauses
# We vigorously handwave the phase transition for 3sat


"""
Benchmark various free ways to solve 3sat
"""

def create_random_ksat(num_variables, num_clauses, k = 3):
    """
    Return a random 3sat clause with num_variable  number of variables and num_clauses clauses

    :param num_variables:
    :param num_clauses:
    :param k: k in ksat
    :return: A list of K-tlists of variables. Each variable is tuple contains a pair, which is an integer (the name of the variable)
    and whether or not it is negated. This is a 3sat clause,in CnF
    """
    def valid(clause):
        return len(set(var for var, _ in clause)) == len(clause)
    def create_clause():
        while True:
            clause = tuple((random.choice(range(num_variables)), random.random() < .5) for i in range(k))
            if valid(clause):
                return clause

    clauses = set()
    while len(clauses) < num_clauses:
        new_clause = create_clause()
        while new_clause in clauses:
            new_clause = create_clause()
        clauses.add(new_clause)

    return list(clauses)

def evaluate(cnf, variables):
    return all(any(variables[name] == val for name, val in clause) for clause in cnf)

def get_num_symbols(sat_instance):
    return max(max(tup[0] for tup in clause) for clause in sat_instance) + 1

def canonical_solver(sat_instance):
    """
    Reference solver. Assume complete and sound.
    :param sat_instance:
    :return:
    """

    num_symbols = get_num_symbols(sat_instance)
    symbols = [Symbol(str(i)) for i in range(num_symbols)]
    domains = [Or([Iff(Bool(is_true), symbols[variable]) for variable, is_true in clause]) for clause in sat_instance]

    formula = And(domains)

    model = get_model(formula)
    if model:
        return True
    else:
        return False

def assignment_from_num(i, num):
    return [bool((i >> index) & 1) for index in range(num)]

def nonconvex_local(sat_instance):
    n = get_num_symbols(sat_instance)

    def cost(x):
        return [sum(
            min(int(1 - x[variable]) if is_true else int(x[variable]) for variable, is_true in clause)
            for clause in sat_instance
        )
        ]

    results = []

    for i in range(10):
        start = [int(random.random() < .5) for i in range(n)]
        result = minimize(cost, start, bounds = [(0, 1) for i in range(n)])

        guessed_output = [int(a >= 0.5) for a in result.x]

        results.append(evaluate(sat_instance, guessed_output))

    return any(results)

def hyperopt(sat_instance):
    n = get_num_symbols(sat_instance)
    def cost(x):
        return sum([
            min(int(1 - x[variable]) if is_true else int(x[variable]) for variable, is_true in clause)
            for clause in sat_instance
        ])
    c = 2.1
    best = fmin(fn=cost,
                space=[hp.randint('x' + str(i), 0, 2) for i in range(n)],
                algo=tpe.suggest,
                max_evals = 2 * int(n ** c))

    return cost(list(best.values())) < 1

def brute_force(sat_instance):
    """
    Solve in Exponential time. For fun. O(c * (2 ** n))
    :param sat_instance:
    :return:
    """
    def all_instances(num):
        for i in range(2 ** num):
            yield assignment_from_num(i, num)
    return any(evaluate(sat_instance, s) for s in all_instances(get_num_symbols(sat_instance)))

def do_benchmark() -> pd.DataFrame:
    solution_strategies = {"canonical":canonical_solver, "ilp": do_cbc_solver, "schonig": schonig,
                           "crank_algorithm": crank_algorithm, "local_sat": local_sat,
                           "brute_force": brute_force, "nonconvex_local": nonconvex_local, "hyperopt": hyperopt}
    hit_cutoffs = set()
    ns = [int(a / REPEATS) for a in range(MIN_N * REPEATS, MAX_N * REPEATS, 1)]
    cols = collections.defaultdict(list)

    for n in ns:
        new_row = dict()
        new_row["n"] = n
        instance = create_random_ksat(n, int(n * critical_ratio))
        for solution_name, solution in solution_strategies.items():
            start = time.time()
            new_row[solution_name] = solution(instance) if solution_name not in hit_cutoffs else False
            end = time.time()
            new_time = end - start
            new_row[solution_name + "_time"] = new_time
            if new_time > TIMEOUT:
                hit_cutoffs.add(solution_name)
        right_solution = new_row["canonical"]

        for solution_name in solution_strategies:
            if solution_name in hit_cutoffs:
                new_row[solution_name + "_correct"] = False
            else:
                new_row[solution_name + "_correct"] = right_solution == new_row[solution_name]

        for key in new_row:
            cols[key].append(new_row[key])

    return pd.DataFrame(cols)

def do_cbc_solver(sat_instance):
    n = get_num_symbols(sat_instance)

    m = Model("knapsack", solver_name = CBC)

    x = [m.add_var(var_type=BINARY) for i in range(n)]

    for clause in sat_instance:
        m += xsum(x[var] if is_true else 1 - x[var] for var, is_true in clause) >= 1

    status = m.optimize()

    return status == OptimizationStatus.OPTIMAL or status == OptimizationStatus.FEASIBLE


def schonig(sat_instance):
    """
    Schonig's algorithm
    :param sat_instance:
    :return:
    """
    n = get_num_symbols(sat_instance)

    def attempt_greedy_walk():
        randomized_assignment = [random.random() < .5 for i in range(n)]
        c = len(sat_instance)
        for i in range(5 * c):
            evaluation = evaluate(sat_instance, randomized_assignment)
            if evaluation:
                return True
            for clause in sat_instance:
                if not evaluate([clause], randomized_assignment):
                    var, _ = random.choice(clause)
                    randomized_assignment[var] = not randomized_assignment[var]
                    break

        return False


    return any(attempt_greedy_walk() for i in range(10))

def local_sat(sat_instance):
    """
    Gradient descent esque sat, with some simulated annealing. Should be worse than schonig better better than the crank
    :return:
    """
    """
    Schonig's algorithm
    :param sat_instance:
    :return:
    """
    n = get_num_symbols(sat_instance)

    map = [0] * n

    for clause in sat_instance:
        for variable, is_true in clause:
            map[variable] += 1 - (2 * is_true)

    def attempt_greedy_walk():
        randomized_assignment = [random.random() < .5 for i in range(n)]
        c = len(sat_instance)
        for i in range(5 * c):
            evaluation = evaluate(sat_instance, randomized_assignment)
            if evaluation:
                return True
            for clause in sat_instance:
                if not evaluate([clause], randomized_assignment):
                    var, _ = max(clause, key = lambda tup: ((map[tup[0]] if not randomized_assignment[tup[0]] else -map[tup[0]]), random.random()))
                    randomized_assignment[var] = not randomized_assignment[var]
                    break

        return False


    return any(attempt_greedy_walk() for i in range(30))


def crank_algorithm(sat_instance):
    """
    If this works the following author is a millionare, and P = BPP
    https://arxiv.org/ftp/arxiv/papers/1703/1703.01905.pdf
    :param sat_instance:
    :return:
    """

    n = get_num_symbols(sat_instance)
    # M is some free parameter less than n, lets fix arbitrarily
    M = n - 1
    # For some reason M is assumed to be even
    if M % 2:
        M = M - 1

    M = 4

    current_assignment = [int(M / 2) for i in range(n)]

    def evaluate_fractional_clause(clause, variables):

        k = len(clause)
        out = 0
        for subset in range(1, k + 1):
            mult = (-1) ** (subset + 1)
            for combo in combinations(range(k), subset):

                out += reduce(mul,(((variables[clause[i][0]]) if clause[i][1] else (M - (variables[clause[i][0]] / M))) for i in combo)) * mult / (M ** subset)

        return out

    def worst_clause_and_val():
        return min(((clause, evaluate_fractional_clause(clause, current_assignment)) for clause in sat_instance), key = lambda a: (a[1], random.random()))

    for i in range(20 * n * n * M * M):
        assert all(var <= M for var in current_assignment)
        worst_clause, worst_clause_truth_value = worst_clause_and_val()
        if worst_clause_truth_value == 1:
            return True
        else:
            random_var, _ = random.choice(worst_clause)
            increments = {0.0: [1], M: [-1]}
            increment_choice = random.choice(increments.get(current_assignment[random_var], [1, -1]))
            current_assignment[random_var] += increment_choice

    return False



benchmark_df = do_benchmark()

# print(do_cbc_solver(create_random_ksat(10, 100)))

benchmark_df.to_csv("data", index = False)
benchmark_df.groupby("n").mean().to_csv("data_grouped", index = True)

pd.set_option("display.max_rows", None, "display.max_columns", None, "display.width", 1000)
print(benchmark_df)
print(benchmark_df.groupby("n").mean())

# print(benchmark_df)
        

Abstract Nonsense

"Abstract Nonsense" is a somewhat loving, but somewhat derisive term for methods (typically Category Theoretic methods) in pure mathematics that are unreasonably convoluted and involve a lot of theoretical machinery. I myself am awful at Category theory but excellent at abstract nonsense, and I wanted a space to share my thoughts and projects. I'm well aware that very few people will read this blog, but to me this space is a journal. A respite from the giants that control the web, and a space to share my thoughts into the void, in a way I can control and moderate.


More concretely, I hope to maintain "Abstract Nonsense" as a dev log as sorts. Not because I think it showcases phenomenal technical talent, but because it showcases some of the cool things I've been learning on the side.


I'll keep my first entry on this journal quite short. This entry stands well on its own. Because it does something the category theorist in all of our hearts would love.


It's self referential.


The content engine that runs Abstract nonsense is quite brilliant if I do say so myself. It is a python script tha takes in a series of html files, and agglomerates them into a single file.


In addition to the abstract nonsense engine I have two other python scripts that form the backbone of this (static) website. I have a script that takes in plaintext of a quote document I have been personally maintaining for the past 3 years. It uses regular expressions to parse out the quotes and build an html file that contains java-script that builds a dynamic webpage this java script program alters the html on the page to create a typing effect. Check it out here! The final piece of this beautiful infrastructure is a third script that runs both scripts than commits the whole branch to master.


As I learned on Twitter/Reddit/The Quote Document: "Everybody has a testing environment. Some people are lucky enough enough to have a totally separate environment to run production in." - @stahnma Abstract nonsense and this website as a whole is both test and prod. Maybe one day, I'll be a good enough engineer to be able to invest in a test and prod for my website.

Housing Spreadsheet

This is a simple standalone web that will help you to think through different homebuying scenarios. It helps model the implications of financing a home with a given fixed rate mortgage and selling the home at the end of the period.

Definitions

Optimizer

If you have a fixed budget or you want to tweak the numbers to see what would need to change to meet certain financial goals try out the optimizer. The optimizer uses the bisect method to find some input which meets a certain goal. For example, say you have 100,000$ and you want to figure out how much you can spend on a house, the optimizer will help you budget.


Future Work

Right now this product is in a tech-demo stage. Short-term, there are two features that we plan to build out relatively shortly.

Long-term we also want to add a few more features.

Housing calculator

Free Ultramarathon

This is a weird blog entry. The end goal of this project is to eventually run a 100 mile Backyard Ultramarathon using only free software This rule is to be interpreted as reasonably as possible and should only apply to tech worn or carried through the race. This rule also does not apply to any crew. This rule is to be followed in spirit. For example if unavoidable small bits of nonfree cpu microcode are acceptable or in modem firmware, care will be taken to isolate such components. An artifact of this is any music listened to during the race will be DRM-Free. The patent on mp3s has recently expired so it is free. I've been a pretty rubbish runner for most of my childhood so this project is technically and physically grueling.

Challenges

Progress

My goal is to be a 95th percentile runner across a range of distances from 1 mile to the 100 Mile run and have at least one P99 performance before my 25th birthday. Some of these numbers are rough estimates. Others are obtained from public data Update 2024-05-27. I am going into my second-ever ultramarathon, and I do not yet have a prototype device that is compliant with the constraints of this challenge. However, it should be an interesting race. To track my progress, read more here.
Distance P95 P99 PR
Mile 6:00 5:20 5:47*
1.5 mi 9:10 8:22 8:58*
5k 21:12 17:38 19:47*
10k 41:17 34:24 44:42
Half Marathon 1:33:04 1:18:07 1:38:13
Marathon 3:08:42 2:44:18 3:58:05
50k ??? ??? 4:56:35
24 hr Backyard ultra ruleset run distance 50 mi 100 mi 34.4 mi

Dev Log

This page will also be a dev-log of progress on mobile/embedded dev projects that build towards the above goals. I've acquired a watch that runs free software, so I am practicing embedded development on it. There are interesting optimizations that you need for embedded dev that would sound horrible anywhere else. For example, we do business logic for the game on the graphics buffer directly... We provide the source here. In honor of Richard Stallman, the code is offered both under an Affero GPL v3 (or later) license, or the MIT license for this whole site.
Source
        
var counter = 30;
var counterInterval;

E.setFlags({pretokenise:1});

gameOver = false;

var stop = false;
var score = 0;
STANFORD_COLOR = 182;
SCREEN_SIZE= 240;
MIDDLE = SCREEN_SIZE >> 1;
BOARD_HEIGHT = 24;
BOARD_WIDTH = 12;

TETRIS_FILL = BOARD_WIDTH;

SQUARE_SIZE = 8;
X_SQUARES = SCREEN_SIZE / SQUARE_SIZE;
Y_SQUARES = SCREEN_SIZE / SQUARE_SIZE;

START_X = (X_SQUARES - BOARD_WIDTH) / 2;
START_Y = (Y_SQUARES - BOARD_HEIGHT) / 2;

colors = [0x000000, 16, 204, 51, 162];
// Long, S,  Box, T, L, Right handed L, trimino, monomino
pieces = [[4, 15 << 4], [3, 51], [2, 15], [3, 23], [3, 15], [3, 39], [3, 56], [1,1]];

function getBit(n, b){
  "ram";
  // assumes n is a 32 bit integer. UB otherwise.
 return (n & (1 << b)) >> b;
}


function setBit(n, b, val){
  "ram";
  // assumes n is a 32 bit integer. UB otherwise.
 return (n | (val << b));
}

function rotate(piece){
 /* Rotate piece 90 degrees counter clockwise */
  // yeah yeah,. there's a better way
  // math math.
  var len = piece[0];
  if(piece[0] == 2){
  return piece;
  }
  var new_locs;
  if(piece[0] == 4){
  new_locs = [12, 8, 4, 0, 13, 9, 5, 1, 14, 10, 6, 2, 15, 11, 7, 3];
  }else{
   new_locs = [6, 3, 0, 7, 4, 1, 8, 5, 2];
  }

  var out = 0;

  for(var i = 0; i < len * len; i++){
  out = setBit(out, new_locs[i], getBit(piece[1], i));
  }

  return [piece[0], out];


}

function rotateOptions(piece){
  var out = [piece];
  for(var i = 0; i< 3;i++){
    out[i + 1] = rotate(out[i]);
  }
  return out;
}
pieces = pieces.map(rotateOptions);


function check(buff, x, y){
  "ram";
  return  buff[(y + START_Y) * Y_SQUARES + (x + START_X)];
}

function set(buff, x, y, val){
"ram";
  buff[(y  + START_Y) * Y_SQUARES + (x + START_X)] = val;
}


function getRandomPiece(){
  "ram";
  return [colors[ 1 + Math.floor(Math.random()* (colors.length -1))],
                 pieces[Math.floor(pieces.length * Math.random())], BOARD_WIDTH >> 1 - 2, 0, 0];
}

current_piece = getRandomPiece();


function assignValuesToPiece(piece, colorMultiplier){
  "ram";
  var len = piece[1][0][0];
  for(var i = 0; i< len; i++){
    for(var j = 0; j< len; j++){
      x = piece[2];
      y = piece[3];
      piece_bm = piece[1][piece[4]][1]
      color = piece[0] * colorMultiplier;
      if(getBit(piece_bm, j * len + i)){
        set(board, x + i, y + j, color);
        }
    }
  }
}

function getBoard(){
  const img = new Uint8Array(X_SQUARES * Y_SQUARES).fill(STANFORD_COLOR);
  for(var i = 0; i < BOARD_HEIGHT; i++){
  for(var j = 0; j < BOARD_WIDTH; j++){
      img[(i + START_Y) * Y_SQUARES +  j + START_X] = 0;
    }
  }
  return img;
}

var board = getBoard();

function drawBoard(board){
  "ram";
  const imgObj = {width: X_SQUARES, height: Y_SQUARES, bpp: 8,
                  buffer: board, msb: true};
  g.drawImage(imgObj, 0, 0, {scale: SQUARE_SIZE});


  g.setFontAlign(0,0); // center font
  g.setFont("6x8",1.5); // bitmap font, 8x magnified
  g.setColor(-1).drawString("Score:", 210, 112);
  g.setFontAlign(0,0); // center font
  g.setFont("6x8",2.5); // bitmap font, 8x magnified
  g.setColor(-1).drawString(score, 210, 130);
}

function isValidPlacement(piece){
  "ram";
  len = piece[1][0][0];
  console.log(len);
  console.log(piece);


  for(var i = 0; i< len; i++){
    for(var j = 0; j< len; j++){
      x = piece[2] + i;
      y = piece[3] + j;
      pieceSet = getBit(piece[1][piece[4]][1], j * len + i);

      if(pieceSet){
      inBounds = x >= 0 && x < BOARD_WIDTH && y >= 0 && y < BOARD_HEIGHT;
      invalid = pieceSet != 0 && (!inBounds || (check(board, x, y) != 0));

      if(invalid){
      return false;
      }
      }
    }

}
      return true;
}



function onlyFall(piece){
  "ram";
    // TODO: implement rotation ?
  return [piece[0], piece[1], piece[2], piece[3] + 1, piece[4]];
}
function updatePiecePlacement(piece){
  dx = 0;
  dx += BTN1.read() || BTN4.read()? -1 : 0;
  dx += BTN3.read() || BTN5.read() ? 1 : 0;

  return [piece[0], piece[1], piece[2] + dx, piece[3] + 1, (piece[4] + (BTN2.read() ? 1 : 0)) & 3];

}

function countLastRow(n){
  "ram";
  sum = 0;
  for(var i = 0; i< BOARD_WIDTH; i++){
   sum += !!check(board, i, n);
  }
  return sum;
}


function updateBoard(){
  "ram";
  score += 1;
  assignValuesToPiece(current_piece, 0);
  var new_piece = updatePiecePlacement(current_piece);
  if(isValidPlacement(new_piece)){

    current_piece = new_piece;
    assignValuesToPiece(current_piece, 1);
  } else {
     var new_piece_fall = onlyFall(current_piece);
  if(isValidPlacement(new_piece_fall)){
    assignValuesToPiece(current_piece, 0);
    current_piece = new_piece_fall;
    assignValuesToPiece(current_piece, 1);
  } else {
    assignValuesToPiece(current_piece, 1)
    extra = 0;

    var keep = Array(BOARD_HEIGHT).fill(0);

    for(var i = 0; i < BOARD_HEIGHT ; i++){
     if(countLastRow(i) >= TETRIS_FILL){
       extra += 1
       score += 10;
     } else {
       keep[i] = 1;
     }

    }

    if(extra > 0){
      newBoard = getBoard();
      count = 0;
      for(var i = 0; i< keep.length; i++){
        if(keep[keep.length - i]){

          var h_new = BOARD_HEIGHT + START_Y - count -1;
          var h = BOARD_HEIGHT + START_Y - i;
        slice = board.subarray((h) * Y_SQUARES, (h + 1) * Y_SQUARES);
        newBoard.set(slice, Y_SQUARES * h_new);
        count += 1
        }
      }
      board = newBoard;
    }

    current_piece = getRandomPiece();

    if(!isValidPlacement(current_piece)){
       gameOver = true;
       }


  }
  }
}

function drawBg(){
  "ram";

}

function gameOverScreen(){
g.setFontAlign(0,0); // center font
g.setFont("6x8",3); // bitmap font, 8x magnified
  g.setColor(-1).drawString("Game Over!", MIDDLE, MIDDLE);
 stop = true;
}

function tetris() {
  "ram";

  if(stop){
  return;
  }

  drawBoard(board);
  if(!gameOver){

  updateBoard();
  }
  else{
    gameOverScreen();
  }
  Bangle.setLCDPower(1);
}

function loop() {
  "ram";
  tetris();
  setTimeout(loop, 100 - (score >> 4));
}



g.clear();
loop();


        

GPT 9001/Abstract Nonsense

This "blog" is called "Abstract Nonsense" because of this project. Most language models try to build interesting output, but end up spouting abstract nonsense (with or without some semantic correctness). Well, I thought to myself, I have a corpus that itself is really just abstract nonsense, maybe I could train an NLP transformer model on this corpus, and oddities of syntax, would actually be a feature!


Because the robot is confused, it will also be named Abstract Nonsense, to maximize perplexity with respect to the identically named blog hosted on this site


I present to you GPT 9001! Which is really just a fine tuned version of GPT 2 tuned for text generation on the Quote Doc In this project I learned that hand-rolled models that I can quickly train are trash. For example, the first implementation of GPT 9001, was called GPT0, and was just some LSTM model I spun up and trained on the quote doc, the LSTM model could either predict random words or overfit the training set. It couldn't do anything of interest :(.


Anyway, without further ado here s/he is:






Here GPT 9001 is reflecting on the repetitive nature of training deep neural networks. Quite introspective, and certainly not just a chance occurrence! Click the image or this sentence to see more brilliancies from GPT 9001 Please understand that the writings on this page are that of an AI and despite a good faith set of filters might be unsettling, mildly profane, or nonsense. GPT was pre-trained on a corpus of data, so a name appearing in its output does not necessarily mean I know this person. The model also predicted authors. These predictions are quite funny especially if you know the people, but to avoid people mistaking satire for reality, I will not show the names. Update: new and improved model (GPT 3 based)

Bidya Ultramarathon

This is the official page for tracking my (Rohan Jhunjhunwala's) progress and funds raised during his Backyard Ultramarathon for Bidya.

Bidya is an organization which raises money to create scholarships for underprivileged females in Nepal. With as little as 1500-2500$ in capital we can create a scholarship fund which can fund all annual K-12 educational expenses for one Female student in need using the interest returns alone.

Because of the comparatively low costs in Nepal, and our relationships with certain high-schools, we can ensure that every dollar Bidya fundraises will efficiently go to a child in need.

Donations to Bidya are 100% 501c(3) tax deductible. Rohan and Rakchhya are matching all donations made to this Ultramarathon fundraiser. For every dollar donated, 3$ will go to funding critical scholarships for underprivileged female Nepali students. To make a per-mile pledge reach out to rjhunjhunwala80@berkeley.edu or feel free to donate directly.

This is a race without a finish line. Competitors run 4.17 miles every hour on the hour until there is just one athlete left standing able to complete the loop. Any pledge, big or small, makes a big difference both to our scholars and to me when I'm exhausted out on the course hoping to be the last man standing. As a thank you to our patrons. I will update this page live during the race, Saturday, June 1. The javascript graph below will track the total funds raised so far. The race also has an official Facebook Leaderboard. If you'd like to drop some cheers in the comments there, we'd be really appreciative. Special thanks to all supporters and my team that is coming out to this event.

Thank you to our current pledges and donations (listed anonymously).

  1. 500$ + Matching all remaining donations 1:1
  2. A second match of all remaining donations 1:1
  3. 500$ flat contribution
  4. (2 pledges) 1$ per mile for the first 25, 2$ for the next 25, 3$ each for the next 25 and so on.
  5. 1$ per mile for the first 50, 2$ per mile for the next 50, 3$ per mile for the 3rd 50 miles. Losing it all if I go over.
  6. (2 pledges) 1$ per mile for the first 50, 2$ for any remaining miles
  7. 2.5$ per mile
  8. 100$ flat contribution

Money raised (inclusive and exclusive of matching funds) As a function of miles run.


Pats for a good floofer!

This update is a quick one.

I learned that this floofer needed some head pats, and I had to help!

This is an important cause, so feel free to compile and run the following java script (not javascript fortunately) to help out the floofer.

Help the floofer with this script!
        
package none;

import java.awt.Color;
import java.awt.Desktop;
import java.awt.MouseInfo;
import java.awt.Point;
import java.awt.Robot;
import java.awt.event.InputEvent;
import java.net.URI;
import java.util.Calendar;
import java.util.Random;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 *
 * @author rohan
 */
public class PetFloofer {

	/**
	 * @param args the command line arguments
	 */
	public static void main(String[] args) throws Exception {
        Thread.sleep(3000);
		int NUM_PETS = 25;
		int pause = 334;
		Robot robot = new Robot();
		int steps = 334;
		int startX = 780;
		int endX = 1150;
	    double stepSize = ((double) (endX - startX) / steps);
		for(int i = 0;i<=NUM_PETS-1;i++){
            for(int step_num = 0;step_num<=steps-1;step_num++){
            int x = (int) (startX + step_num * stepSize);
            robot.mouseMove(x, 400);
            Thread.sleep(pause/steps);
            }
		}

		}

	}
        
Execution instructions
        javac PetFloofer.java && java PetFloofer.java
Download the source here!

pip install pandas

Pandas is a leading library in the field of data science, when you utter the magic words:
Spell

pip install pandas
    
You get a powerful library to explore, analyze, and transform massive data sets using expressive syntax.


You even get chills as you type the commands into your terminal:
Magical application
python my_magic_app.py
    

Your app runs, it does the big data, but still... somethings missing... you can't put your finger on it....


You are missing ACTUAL pandas!! Wouldn't it be great if these magic spells also summon the animals whose name you invoke? Introducing: pipinstallpandas.py! Whenever you invoke the name (or even mention it in any context of an animal to do your magical programming work, this script will also show you some pictures of the cuties to help you properly express your gratitude some example commands to try in your terminal. Typing other words will show you a surprise.
Supported commands

python pipinstallpandas.py # start the logger
conda install tensorflow
pip install pandas
python my_amazing_app.py >> output_log.txt
cat output_log.txt
    
Without further ado: here is the script:
Source
        
from pynput.keyboard import Key, Listener
import time
import random

from selenium import webdriver
from selenium.webdriver.common.keys import Keys

mutable_st = []


from subprocess import Popen, check_call

def check(mutable_st, key):
    l = len(key)
    return len(mutable_st) >= l and all(mutable_st[i - l] == key[i] for i in range(len(key)))


def open_then_close(url, time_to_sleep = 3):
    browser = webdriver.Chrome()
    browser.get(url)

    time.sleep(time_to_sleep)

    browser.close()

def on_press(key):
    try:
        mutable_st.append(eval(str(key)))
        print(mutable_st[-1])
    except:
        pass
    do_nothing_function = lambda : None

    def get_random_picture_of(thing):
        adjectives = ["cute", "cuddly", "floofy", "soft",
                      "adorable", "big", "aww", "safe",
                      "happy", "sad", "tame"]
        random.shuffle(adjectives)
        adjectives_to_use = []
        for adjective in adjectives:
            if random.random() < .5:
                adjectives_to_use.append(adjective)
        query_words = adjectives_to_use + [thing]
        query = "+".join(query_words)
        open_then_close("https://www.google.com/search?q={}&source="
                        "lnms&tbm=isch&sa=X&ved=2ahUKEwjFhauqu4HwAhW"
                        "VElkFHcX7CPgQ_AUoAXoECAEQAw&biw=1745&bih=881".format(query))

    quit = lambda : exit(0)
    keywords = {"python": lambda : get_random_picture_of("pythons"),
                "conda": lambda : get_random_picture_of("cartoonish plush snake"),
                "pandas": lambda : get_random_picture_of("pandas"),
                "floof": lambda : get_random_picture_of("floofers"),
                "dog": lambda : get_random_picture_of("dog"),
                "cat": lambda : get_random_picture_of("cat"),
                "fuck": lambda : get_random_picture_of("great alaskan malamute"),
                "shit": lambda : get_random_picture_of("giant flemish rabbit"),
                "sad": lambda : get_random_picture_of("hug"),
                "leavelogger": quit}

    for key, function in keywords.items():
        if check(mutable_st, key):
            function()

with Listener(on_press=on_press) as listener:
    listener.join()
        
Download the script here. Formatting for code borrowed from this Code Pen See on Github

Solving wordle (poorly) using overly sophisticated algorithms and no machine structures.

I came across an exciting problem in a stand up maths video.

Using a simple brute force graph-theory argument, a viewer had gotten the runtime of Matt's solution down from 32 days to 15 minutes. By throwing the book at the problem I thought we could do better. With good fundamental knowledge of the english language and machine structures other authors have implemented some variant of exhaustive search with substantially better runtime of 100 milliseconds. With fundamentally simple code. However, using Mixed integer programming, ( a simple formulation around set covering) we can optimize this to 10 seconds (360 * 24 * 32) times faster than Matt's code. An alternate approach using pySMT (satisfiability modulo theories) has an estimated runtime of around 11 hours. My formulation of this as a SMT problem finds one of the 11 assignments of words for this problem 1 hour. These are overkill solutions but have a certain mathematical elegance to them, that makes me really happy.

Help the floofer with this script!
        
            import pysmt as pysmt
import sys
from pysmt.shortcuts import SBV, Symbol, is_valid, Equals
from pysmt.typing import BV32

from pysmt.shortcuts import Symbol, Or, And, GE, LT, Plus, Equals, Int,  get_model, BV
from pysmt.typing import INT

import time

import mip

from mip import Model, xsum, maximize, BINARY, OptimizationStatus, ConstrsGenerator, GRB, CBC

from collections import Counter

if len(sys.argv) == 2:
    print("here!")
    dic = sys.argv[1]
else:
    dic = "wordle_guesses.txt"

ALPHABET = "abcdefghijklmnopqrstuvwxyz"

WORDLE_LEN = 5
CHARS = 5

with open(dic) as fh:
    WORD_LIST = list(set([word.strip() for word in fh.readlines() if len(word.strip()) == CHARS and CHARS == len(set(word.strip()))]))




# Too slow: takes one hour
# TODO: figure out how to get all solutions (solution re-run with additional constraints. SOlution counting is known
# to be #P complete, so not much too do but have runtime rpoporational to number of solutions
def get_all_wordle_solutions_mip(dictionary: list[str], blacklist: list[list[str]] = []) -> None | list[str]:
    solutions = set()

    m = Model("Quick milp wordle model. Perf benchmark CBC free solver", solver_name = CBC)

    words = {word:m.add_var(var_type=BINARY) for word in  dictionary}

    m += xsum(word for word in words.values()) == 5

    word_counts = {word: Counter(word) for word in words}

    for ch in ALPHABET:
        m += xsum(words[word] * word_counts[word][ch] for word in words) <= 1

    for solution in blacklist:
        m += get_constraint_from_solution(solution)

    class KeepOnSolving(ConstrsGenerator):
        def generate_constrs(self, model, depth = 0, npass = 0):
            solution = tuple(dictionary[i] for i in range(len(model.vars)) if model.vars[i].x >= .99)
            solutions.add(solution)
            model += xsum(var for var in model.vars if var.x >= .99) <= 4
            print(solution)
            time.sleep(0.25)


    m.lazy_constrs_generator = KeepOnSolving()
    m.infeas_tol = 1e-2
    status = m.optimize(max_seconds = 1000000000000)

    return solutions

def get_bitvec(word: str) -> int:
    out = 0
    counts = Counter(word)
    for i, ch in enumerate(ALPHABET):
        out += counts[ch] << i
    return out

def get_all_solutions_smt(dictionary: list[str]):
    solutions = []



    unique_chars = [word for word in dictionary if len(set(word)) == len(word)]

    bitvecs = [get_bitvec(word) for word in unique_chars]

    def get_one_solution_smt(blacklist: list[list[str]] = []) -> list[str]:
        words = [Symbol("word" + str(i), BV32) for i in range(WORDLE_LEN)]
        domains = And(Or(Equals(word, BV(vec, 32)) for vec in bitvecs) for word in words)


        problem = And(And(Equals(words[i] & words[j], BV(0, 32))for j in range(i)) for i in range(WORDLE_LEN))
        formula = And(domains, problem)

        print("Serialization of the formula:")
        print(formula)

        model = get_model(formula)
        if model:
            print(model)

        return None

    solutions.append(get_one_solution_smt())


    return solutions

def get_one_solution_hardcoded_smt(dictionary: list[str]) -> list[list[str]]:
    """
    Output of hardcoded run
    word4 := 35668104_32
word0 := 656404_32
word1 := 17863168_32
word2 := 10562_32
word3 := 4522017_32

    :param dictionary:
    :return:
    """
    hardcoded = [35668104, 656404, 17863168, 10562, 4522017]
    out = [[]]

    for vec in hardcoded:
        for word in dictionary:
            if len(set(word)) == len(word) and get_bitvec(word) == vec:
                out[0].append(word)
                break

    return out



strategies = [get_all_wordle_solutions_mip, get_one_solution_hardcoded_smt]

for strategy in reversed(strategies):
    solutions = strategy(WORD_LIST)
    print(str(strategy), "found", len(solutions), "solutions")
    for words in solutions:
        print(str(strategy), " Solution: ", *words)


        
Execution instructions
        javac PetFloofer.java && java PetFloofer.java
Download the source here!