Using machine vision to solve industrial Boolean satisfiability (SAT) problems

A computer system for processing industrial Boolean satisfiability (SAT) problems comprising:

• a computer implemented SAT image encoder configured to encode an industrial SAT problem comprising a plurality of clauses into a pixelated problem image comprising a plurality of rows, wherein:
• each row of the pixelated problem image represents a corresponding one of the clauses;
• each row of the pixelated problem image comprises D pixels where D is a total number of variables in the industrial SAT problem;
• and
• each pixel is configured with one of a plurality of weights, including a first weight indicating a positive literal of the corresponding variable, a second weight indicating a negative literal of the corresponding variable, and a third weight indicating the variable is not in the corresponding clause;
• a computer implemented clause embedding module configured to encode each row of the pixelated problem image into a corresponding vector;
• and
• a computer implemented vector encoder configured to encode the vectors into an output indicating whether the industrial SAT problem is satisfiable or unsatisfiable.

A computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor, the method comprising:

• using a computer to encode a training industrial SAT problem into a pixelated problem image comprising a plurality of rows, wherein the training industrial SAT problem comprises a plurality of clauses and each row of the problem image represents a corresponding one of the clauses;
• using the computer to process the pixelated problem image using a computer implemented machine vision module which generates an output indicating whether the training industrial SAT problem is satisfiable or unsatisfiable;
• using the computer to compare the output to a predetermined satisfiability solution of the training industrial SAT problem to generate a training error;
• and
• using the computer to adapt the machine vision module based on the training error.