Fast Analysis of the OpenAI O1-Preview Model in Solving Random K-SAT Problem: Does the LLM Solve the Problem Itself or Call an External SAT Solver?

TL;DR

This paper investigates whether the OpenAI O1-preview model directly solves random K-SAT problems or relies on external solvers, revealing it often calls external solvers and outputs incorrect solutions, raising questions about its problem-solving capabilities.

Contribution

The study provides a detailed analysis of the model's behavior in solving K-SAT problems, highlighting its dependence on external solvers and assessing its apparent intelligence.

Findings

Model calls external SAT solvers to find solutions.

Model often outputs incorrect assignments.

Analysis suggests the model does not truly solve K-SAT independently.

Abstract

In this manuscript, I present an analysis on the performance of OpenAI O1-preview model in solving random K-SAT instances for K$\in {2,3,4}$ as a function of $\alpha=M/N$ where $M$ is the number of clauses and $N$ is the number of variables of the satisfiable problem. I show that the model can call an external SAT solver to solve the instances, rather than solving them directly. Despite using external solvers, the model reports incorrect assignments as output. Moreover, I propose and present an analysis to quantify whether the OpenAI O1-preview model demonstrates a spark of intelligence or merely makes random guesses when outputting an assignment for a Boolean satisfiability problem.