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

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

a computer implemented SAT image encoder configured to encode a runtime industrial SAT problem into a pixelated problem image comprising a plurality of rows, wherein the runtime industrial SAT problem comprises a plurality of clauses and each row of the pixelated problem image represents a corresponding one of the clauses;

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 runtime industrial SAT problem is satisfiable or unsatisfiable.

2 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 1 , wherein the pixelated problem image is permutation invariant.

3 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 1 , wherein the vector encoder comprises a computer implemented self-attention-based encoder.

4 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 3 , wherein the self-attention-based encoder comprises a computer implemented transformer.

5 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 1 , wherein:

each row of the pixelated problem image comprises D pixels where D is a total number of variables in the runtime 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.

6 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 5 , wherein each clause comprises M variables out of the D total variables such that each row comprises D pixels each comprising one of the first weight or the second weight and the remaining pixels in the row each comprising the third weight.

7 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 1 , wherein the runtime industrial SAT problem is one of supply chain management logistics, manufacturing and networking, critical path analysis, floor planning, resource allocation, routing, software verification, or cyber-physical systems verification.

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

9 . The computer implemented system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 8 , wherein each clause comprises M variables out of the D total variables such that each row comprises D pixels each comprising one of the first weight or the second weight and the remaining pixels in the row each comprising the third weight.

10 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 8 , wherein the vector encoder comprises a computer implemented self-attention-based encoder.

11 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 10 , wherein the self-attention-based encoder comprises a computer implemented transformer.

12 . The computer system for processing industrial Boolean satisfiability (SAT) problems as recited in claim 8 , wherein the industrial SAT problem is one of supply chain management logistics, manufacturing and networking, critical path analysis, floor planning, resource allocation, routing, software verification, or cyber-physical systems verification.

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

14 . The computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor as recited in claim 13 , further comprising:

using the machine vision module to encode each row of the pixelated problem image into a corresponding vector; and

using the machine vision module to encode the vectors into an output indicating whether the training industrial SAT problem is satisfiable or unsatisfiable.

15 . The computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor as recited in claim 13 , wherein the machine vision module comprises a self-attention-based encoder.

16 . The computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor as recited in claim 15 , wherein the self-attention-based encoder comprises a computer implemented transformer.

17 . The computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor as recited in claim 13 , wherein:

each row of the pixelated problem image comprises D pixels where D is a total number of variables in the training 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.

18 . The computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor as recited in claim 17 , wherein each clause comprises M variables out of the D total variables such that each row comprises D pixels each comprising one of the first weight or the second weight and the remaining pixels in the row each comprising the third weight.

19 . The computer implemented method of training an industrial Boolean satisfiability (SAT) problem processor as recited in claim 13 , wherein the training industrial SAT problem is one of supply chain management logistics, manufacturing and networking, critical path analysis, floor planning, resource allocation, routing, software verification, or cyber-physical systems verification.