# 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.
• canonical: Standard CDCL type solver from Mathsat
• ilp: Alternate standard way to solve 3Sat via reduction to integer linear programming.
• crank_algorithm: Alleged bounded error polynomial time algorithm for 3sat, found from this paper.
• schonig: The gold standard for heuristic local 3Sat algorithms: Schonig's algorithm
• local_sat: Greedy gradient descent type approach to 3sat.
• nonconvex_local: Assume that the minimization solver from scipy can solve arbitrary nonconvex problems, then reduce 3sat to a nonconvex problem.
• hyperopt: Use black box optimization techniques.
• brute_force: Try every assignment of variables.
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.

### 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.

## 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.

## 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)

# 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.