CN115334019B - Data processing method and programmable switch for handling SAT problem by programmable switch - Google Patents

Abstract

The present disclosure provides a data processing method for a programmable switch to handle SAT problems, which includes: the programmable switch receives SAT formula data preprocessed by the server; the programmable switch receives solving instructions sent by the server; the programmable switch solves the SAT problem; The programming switch sends the SAT problem solving results to the server. The present disclosure also provides a programmable switch.

Description

Data processing method and programmable switch for handling SAT problem by programmable switch

Technical field

The present disclosure relates to the technical field of computer data processing, and in particular, the present disclosure relates to a data processing method and a programmable switch for processing SAT problems by a programmable switch.

Background technique

The Boolean satisfiability problem, or SAT problem for short, is the problem of determining whether there is an explanation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be assigned a value of true or false in such a way that the formula evaluates to true. If it can, then the formula is satisfiable. Otherwise, for a given Boolean formula, the formula is unsatisfiable. The SAT problem originates from the concept of satisfiability of formulas in classical propositional logic in mathematical logic. It is a core problem in computer science and the first problem proven to be NP-complete. It is important in many areas of computer science, circuit design, complexity theory, cryptography, and artificial intelligence.

At present, methods for solving SAT problems are mainly divided into two categories: complete methods and incomplete methods. Incomplete methods can only judge partially satisfiable conjunctive normal forms or judge partially unsatisfiable conjunctive normal forms. For example, local search cannot prove that a conjunctive normal form CNF is unsatisfiable. The complete method can prove that any CNF is satisfied or unsatisfied. For complete SAT solving algorithms, two commonly used algorithms are DPLL algorithm and CDCL algorithm. Early SAT problem solving was mainly based on the DPLL algorithm, which is the basic algorithm for solving SAT problems. Most of the later research was based on the DPLL algorithm; the CDCL (conflict-driven clause learning) algorithm is a modern SAT solver. A commonly used solving algorithm, this algorithm is based on the DPLL algorithm and enhances the basic DPLL search algorithm through effective conflict analysis, clause learning, non-chronological backtracking (aka jumpback), and "double observation text" units.

The time-consuming process of processing SAT problems is mainly focused on determining whether the assignment of a given variable will cause a conflict in the formula (that is, the true value of the formula is false). Its time complexity is O(m*n), where m represents the number of clauses. number, n represents the average number of variables in each clause. Improving the processing speed and efficiency of SAT problems are technical issues that need to be solved urgently.

Contents of the invention

In order to solve at least one of the above technical problems, the present disclosure provides a data processing method and a programmable switch for processing SAT problems in programmable switches (Programming Protocol-independent Packet Processors).

According to one aspect of the present disclosure, a data processing method for a programmable switch to handle SAT problems is provided, including:

The programmable switch receives the SAT formula data preprocessed by the server;

The programmable switch receives the solution instructions sent by the server;

Programmable switches solve SAT problems;

The programmable switch sends the SAT problem solving results to the server.

According to the data processing method of at least one embodiment of the present disclosure, the preprocessing includes: dividing SAT formula data into multiple clauses;

The programmable switch receives the SAT formula data preprocessed by the server, including: the programmable switch puts the multiple clauses into different conflict tables.

According to the data processing method of at least one embodiment of the present disclosure, the solving instructions are sent in the form of data packets, the data packets include control information for solving SAT, and the control information is encapsulated in the form of a packet header, and the packet header includes:

A network type field, which is used to identify the network type to which the SAT solution method is applicable;

Search field, the search field includes control information including assignable variable search, stack operation and unit table matching;

A plurality of judgment fields, each judgment field includes the information of the conflict table and the conflict processing function, the information of the unit table and the unit processing function.

According to the data processing method of at least one embodiment of the present disclosure, the programmable switch solves the SAT problem, including:

Search for assignable variables in the SAT formula data and assign values to the variables in the clauses of the SAT formula data;

Push the assigned variable onto the stack;

Send the variables after assignment to the conflict table, and use the conflict table to determine whether there is a conflict after the variable assignment. If there is a conflict, go back to the stack and reassign the assignable variable. If there is no conflict, proceed to the unit table. match;

Determine whether to generate unit variables based on the matching results of the unit table. If unit variables are generated, assign values to the unit variables. If no unit variables are generated, search for other assignable variables in the clauses of the SAT formula data.

According to the data processing method of at least one embodiment of the present disclosure, determining whether there is a conflict after variable assignment through a conflict table includes:

While assigning values to each variable in the clause of the SAT formula data one by one, determine whether each variable in the clause has been assigned a value through the assignment field of the conflict table;

When the assignment of each variable in the clause of the SAT formula data has been completed, determine whether the assignment of values to the clause of the SAT formula data causes a conflict;

If a conflict occurs, the conflict is handled through the conflict handling function of the conflict table.

According to the data processing method of at least one embodiment of the present disclosure, determining whether each variable of the clause has been assigned a value through the assignment field of the conflict table includes:

Initialize assigned fields to unassigned status information;

After assigning a value to each variable, modify the assignment field corresponding to the variable to the assigned status information;

If the corresponding assignment fields of the clause variables have been modified to the assigned state, it is determined that each variable of the clause has been assigned a value.

According to the data processing method of at least one embodiment of the present disclosure, determining whether to generate unit variables includes:

When each variable in the clause is assigned until only one variable remains unassigned, it is determined that the only remaining unassigned variable is a unit variable.

According to the data processing method of at least one embodiment of the present disclosure, backtracking the stack to find assignable variables is performed through a pointer, and the pointer ensures that the variable currently pointed to and the variables directly or indirectly linked to the current variable through the pointer have completed assignment, so as to Reduce search time for assignable variables.

According to yet another aspect of the present disclosure, a programmable switch is provided, including:

SAT formula data receiving module, the SAT formula data receiving module is used to receive SAT formula data preprocessed by the server;

A solution instruction processing module, which is used to receive the solution instructions sent by the server;

SAT problem solving module, the SAT problem solving module is used to solve SAT problems;

The result sending module is used to send the SAT problem solving results to the server.

According to the programmable switch of at least one embodiment of the present disclosure, the SAT problem solving module includes:

A search component, which is used to search for assignable variables and assign values to the variables;

A judgment component that judges whether the assignment will cause conflicts and whether there are unit variables;

Wherein, the search component is composed of a stack formed by registers and SRAM, and the search component includes:

A search module, which determines assignable variables by traversing all variables, and assigns values to the assignable variables as input to the conflict table;

A rollback module that re-searches assignable variables through the backtrace stack based on the conflict table matching results;

The unit module, based on the judgment result of the unit table, sends a notification to the search module and assigns values to the unit variables if there are unit variables;

Wherein, the judgment component includes a conflict table and a unit table. It is judged based on the conflict table whether the variable assignment to the SAT formula data clause will cause a conflict, and it is judged whether there is a unit variable based on the unit table.

Description of the drawings

The accompanying drawings illustrate exemplary embodiments of the disclosure and together with the description serve to explain the principles of the disclosure, and are included to provide a further understanding of the disclosure, and are incorporated in and constitute part of this specification. part of the instruction manual.

Figure 1 is a schematic flowchart of a data processing method for a programmable switch to handle SAT issues according to an embodiment of the present disclosure.

Figure 2 is an architectural schematic diagram of a programmable switch according to an embodiment of the present disclosure.

Figure 3 is a schematic diagram of a packet header of a programmable switch according to an embodiment of the present disclosure.

Figure 4 is a schematic diagram of a conflict table in the prior art.

Figure 5 is a schematic diagram of a conflict table adding an assignment field according to an embodiment of the present disclosure.

Figure 6 is a schematic diagram of the header structure of the judgment component according to an embodiment of the present disclosure.

Figure 7 is a schematic diagram of a formula dividing method according to an embodiment of the present disclosure.

FIG. 8 is a schematic structural diagram of a unit table according to an embodiment of the present disclosure.

Figure 9 is a schematic diagram of the header structure of a search component according to an embodiment of the present disclosure.

Figure 10 is a schematic diagram of stack operation according to an embodiment of the present disclosure.

Figure 11 is a schematic diagram of the operation of the search component according to an embodiment of the present disclosure.

Figure 12 is a schematic diagram of performance evaluation results of a programmable switch (P4-DPLL) according to an embodiment of the present disclosure.

Detailed ways

The present disclosure will be described in further detail below in conjunction with the accompanying drawings and embodiments. It can be understood that the specific implementations described here are only used to explain the relevant content, but are not intended to limit the present disclosure. It should also be noted that, for convenience of description, only parts related to the present disclosure are shown in the drawings.

It should be noted that, as long as there is no conflict, the embodiments and features in the embodiments of the present disclosure can be combined with each other. The technical solutions of the present disclosure will be described in detail below with reference to the accompanying drawings and embodiments.

Unless otherwise specified, the illustrated exemplary embodiments/examples are to be understood as exemplary features providing various details of some manner in which the technical concepts of the present disclosure may be implemented in practice. Therefore, unless otherwise stated, features of various embodiments/embodiments may be additionally combined, separated, interchanged and/or rearranged without departing from the technical concept of the present disclosure.

The use of cross-hatching and/or shading in drawings is often used to make boundaries between adjacent parts clear. As such, unless stated otherwise, the presence or absence of cross-hatching or shading does not convey or indicate any knowledge of the specific materials, material properties, dimensions, proportions, commonalities between the components shown and/or any other characteristics of the components, Any preferences or requirements for attributes, properties, etc. Furthermore, in the drawings, the size and relative sizes of components may be exaggerated for clarity and/or descriptive purposes. While example embodiments may be implemented differently, a specific process sequence may be performed in a different order than that described. For example, two consecutively described processes may be performed substantially concurrently or in the reverse order of that described. In addition, the same reference numerals represent the same components.

When an element is referred to as being "on," "on," "connected to" or "coupled to" another element, it can be directly on, directly connected to, or directly connected to the other element. Either directly coupled to said other component, or intervening components may be present. However, when an element is referred to as being "directly on," "directly connected to" or "directly coupled to" another element, there are no intervening elements present. For this purpose, the term "connected" may refer to a physical connection, an electrical connection, etc., with or without intervening components.

The terminology used herein is for the purpose of describing particular embodiments and is not intended to be limiting. As used herein, the singular forms "a," "an," and "the" are intended to include the plural forms as well, unless the context clearly indicates otherwise. Furthermore, when the terms "comprises" and/or "includes" and variations thereof are used in this specification, it is stated that the stated features, integers, steps, operations, parts, components and/or groups thereof are present but not excluded. One or more other features, integers, steps, operations, parts, components and/or groups thereof are present or appended. It is also noted that, as used herein, the terms "substantially," "approximately," and other similar terms are used as terms of approximation and not as terms of degree, and as such, they are used to explain what one of ordinary skill in the art would recognize. Inherent deviations from measured, calculated and/or supplied values.

Figure 1 is a schematic flowchart of a data processing method for a programmable switch to handle SAT issues according to an embodiment of the present disclosure.

As shown in Figure 1, the data processing method of programmable switches to deal with SAT problems includes:

S102. The programmable switch receives the SAT formula data preprocessed by the server;

S104. The programmable switch receives the solution instruction sent by the server;

S106, programmable switch solves SAT problem;

S108. The programmable switch sends the SAT problem solving results to the server.

Among them, the server preprocesses the SAT formula data, including: dividing the SAT formula data into multiple clauses.

In this disclosure, the programmable switch places multiple clauses into different conflict tables.

In S104, the solution instructions are sent in the form of data packets. The data packets include control information for solving SAT. The control information is encapsulated in the form of a packet header. The packet header includes:

Network type field. The network type field is used to identify the network type for which the SAT solution method is applicable;

Search field, the search field includes control information including assignable variable search, stack operation and unit table matching;

Multiple judgment fields, each judgment field includes conflict table information and conflict processing functions, unit table information and unit processing functions.

The above-mentioned S106, programmable switch solves SAT problems, including:

Search for assignable variables in the SAT formula data and assign values to the variables in the clauses of the SAT formula data;

Push the assigned variable onto the stack;

Send the assigned variables to the conflict table, and use the conflict table to determine whether there is a conflict after the variable assignment. If there is a conflict, retrace the stack and re-assign the assignable variables. If there is no conflict, match the unit table;

Determine whether the unit variable will be generated based on the matching result of the unit table. If the unit variable is generated, assign a value to the unit variable. If the unit variable is not generated, search for other assignable variables in the clauses of the SAT formula data.

Among them, the conflict table is used to determine whether there is a conflict after variable assignment, including:

While assigning values to each variable in the clause of the SAT formula data one by one, determine whether each variable in the clause has been assigned a value through the assignment field of the conflict table;

When the assignment of each variable in the clause of SAT formula data has been completed, determine whether the assignment of values to the clause of SAT formula data causes a conflict;

If a conflict occurs, the conflict is handled through the conflict handling function of the conflict table.

Among them, the assignment field of the conflict table is used to determine whether each variable of the clause has been assigned, including:

Initialize assigned fields to unassigned status information;

After assigning a value to each variable, modify the assignment field corresponding to the variable to the assigned status information;

If the corresponding assignment fields of the clause variables have been modified to the assigned state, then each variable in the judgment clause has been assigned a value.

Among them, it is judged whether unit variables will be generated, including:

When each variable in the clause is assigned until only one variable remains unassigned, the remaining unassigned variable is judged to be a unit variable.

Among them, the backtrace stack search for assignable variables is carried out through pointers. The pointers ensure that the variables currently pointed to and the variables directly or indirectly linked to the current variable through the pointer have been assigned, so as to reduce the time of searching for assignable variables.

According to yet another aspect of the present disclosure, a programmable switch is provided, including:

SAT formula data receiving module. The SAT formula data receiving module is used to receive SAT formula data preprocessed by the server;

The solution instruction processing module is used to receive the solution instructions sent by the server;

SAT problem solving module, the SAT problem solving module is used to solve SAT problems;

The result sending module is used to enable the programmable switch to send the SAT problem solving results to the server.

According to the programmable switch of at least one embodiment of the present disclosure, the SAT problem solving module includes:

Search component, the search component is used to search for assignable variables and assign values to variables;

Judgment component, the judgment component determines whether the assignment will cause conflicts and whether there are unit variables;

Among them, the search component is composed of a stack formed by registers and SRAM. The search component includes:

Search module, the search module determines assignable variables by traversing all variables, and assigns assignable variables as input to the conflict table;

Rollback module, the rollback module re-searches assignable variables through the backtrace stack based on the conflict table matching results;

The unit module, based on the judgment result of the unit table, sends a notification to the search module and assigns values to the unit variables if there are unit variables;

Among them, the judgment component includes a conflict table and a unit table. It is judged based on the conflict table whether the variable assignment to the SAT formula data clause will cause a conflict, and it is judged whether there is a unit variable based on the unit table.

Figure 2 is an architectural schematic diagram of a programmable switch according to an embodiment of the present disclosure.

As shown in Figure 2, the programmable switch includes a Judgment Component and a Search Component, which use the parallel search capability of the switch to accelerate. In order to avoid the overhead caused by forwarding data packets on the control path, this disclosure deploys both the judgment component (Judgment Component) and the search component (SearchComponent) in the data plane.

The judgment component has two functions. One is to judge whether the current assignment will cause a conflict, and the other is to judge whether the assignment will generate unit variables. These functions are implemented on the programmable switch (P4-DPLL) through two TCAM tables. The first TCAM table is the conflict table (Conflict Table), which is used to determine whether there is a conflict. The second TCAM table is the unit table (Unit Table), which is used to determine whether there are unit variables. The present disclosure achieves acceleration of these two functions by utilizing the parallel lookup capability of the TCAM table.

The main function of the search component is to search for assignable variables, assign values to variables, and handle special situations. A key challenge with the search component is that it requires recording search history for backtracking. In order to cope with this challenge, this disclosure uses registers and SRAM tables to implement a stack structure on the switch, which is also the key design of this disclosure in the search component. The disclosed stack is able to record the search history on the switch and return the correct location when appropriate.

The core of the search component in the programmable switch is a stack that tracks the search history during the SAT solution. Based on this stack, the search component is divided into three parts: search module, fallback module and unit module. The search module and the rollback module operate the stack to complete the forward and backward motion of the algorithm. The unit module does not operate the stack and mainly implements the processing of unit variables.

Since the search component is complex, this disclosure implements it by looping the packets multiple times over a programmable switch. This disclosure uses the OP field to identify what the programmable switch should do when processing the packet, and uses IF_OP_DONE to indicate whether the current operation is over. Control information such as the OP field of the search component is mainly placed in the SEARCH header, as shown in Figure 9.

Referring to Figure 2, in the search module (Search Part), the programmable switch will linearly search all current variables to find assignable variables. To avoid starting the search from scratch every time, the programmable switch maintains a search pointer and ensures that all variables before the pointer have been assigned a value. After finding an assignable variable, the programmable switch assigns its value and generates the input to the conflict table. After completing these operations, the search module pushes the data onto the stack and passes the data to the conflict table.

The Go-back Part is shown in Figure 2 . After the packet is sent to the conflict table, the packet will enter the fallback module. In this part, the solver decides whether to start backoff processing or start looking for cell variables based on the conflict table match. If a return process begins, the solver will continue to backtrack on the stack and reassign variables until there are no more conflicts. If the switch keeps returning until there are no variables to choose from, the solver will report UN-SAT to the server, UN-SAT indicating unsatisfiable. If there are no conflicts, the solver will start matching the Unit Table.

The unit part is shown in Figure 2 . This part of the solver will determine whether the current variable will generate a unit variable based on the results of the unit table. If so, the unit module will report to the search module (it is worth noting that sometimes there are multiple unit variables; in the solver of the present disclosure, the first found unit variable will be selected) and start assigning values to the unit variables. If no unit variable is generated, the programmable switch modifies the OP field, returns to the first part, and looks for the next variable that can be assigned a value.

Figure 3 is a schematic diagram of the packet header data structure of a programmable switch according to an embodiment of the present disclosure.

As shown in Figure 3, in order to carry the data required by the SAT solver, this disclosure designs two dedicated headers, namely SEARCH and JUDGMENT. The programmable switch field is located within the Ethernet payload, so this disclosure also reserves a special Ether Type for programmable switches, namely ETH shown in Figure 3. The switch uses this type to invoke custom packet processing logic.

Figure 4 is a conflict representation diagram of the SAT problem in the prior art.

In SAT formula data, if an assignment causes a conflict, it must be because there is a clause that evaluates to false under the current assignment. For a clause of SAT formula data, evaluates to false, meaning that all characters in the clause evaluate to false. So no matter how long a clause is, there is only one assignment that causes the clause to evaluate to false, which is called a false assignment.

In the formula on the left side of Figure 4, for the first clause, the truth value of the clause is false only if x1 is assigned false, x2 is assigned false, and x3 is assigned true. For the second clause, this clause is false only if x2 is assigned false and x3 is assigned false. Use 0 to indicate that the variable is assigned a false value, and 1 to indicate that the variable is assigned a true value. Because the second clause does not contain x1, the value of x1 is recorded as *, indicating any value. This way, false assignments can be generated for each clause. By analogy, we can get the false assignment of this formula. For any SAT formula, the corresponding false assignment can be obtained.

If a false assignment occurs in an assignment, it can be concluded that the assignment will cause a conflict. A conflict assignment matching table can be constructed based on the false assignment, which is called a conflict table.

As shown in Figure 4, the key of the conflict table is the value of the variable, each bit represents a variable, the action used is the conflict handling function, and each item of the conflict table corresponds to the false assignment of a clause. In this way, as long as the conflict table hits, at least one clause's false assignment must appear in the variable truth assignment of the current formula. Therefore, as long as the conflict table hits, it can be asserted that the current assignment will cause a conflict, so that conflict handling can be transferred. However, this is not enough for the DPLL algorithm. Since the DPLL algorithm assigns values to variables one by one, and the initial value of the variables is 0, directly using the conflict table for matching may get some wrong results.

Figure 5 is a schematic structural diagram of a SAT conflict table with an added assignment field according to an embodiment of the present disclosure.

As shown in Figure 5, when x1 is assigned false, but x2 and x3 have not yet been assigned a value, the key-value is 000, and the second row of the conflict table will be hit, thus turning to conflict processing. However, only x1 is assigned at this time, so no conflict will occur.

In order to deal with this problem, this disclosure adds a key field as assigned in the conflict table, as shown in Figure 5. The assignment field, that is, the assigned field, is used to mark the variables that need to be assigned in the current clause, so as to accurately match whether the false assignment of the current clause appears in the current assignment, where 1 means assigned and 0 means not assigned. Taking the formula in Figure 4 as an example, when x1 is assigned a value of 0, but x2 and x3 have not yet been assigned a value, the value of key-value is 000 and the value of key-assigned is 100, which will not hit anything in the conflict table. entry. It can be seen that by adding the assigned field, accurate matching of false assignments in the current assignment can be achieved.

Figure 6 is a schematic structural diagram of the header of the judgment component according to an embodiment of the present disclosure.

As shown in Figure 6, in order to carry variable information to match the conflict table, the present disclosure uses the judgment component header structure as shown in Figure 6. Limited by the computing power of the programmable switch, the present disclosure sets the length of the VALUE and ASSIGNED fields to 32 bits, which is exactly the upper limit of the switch length to perform computing operations. There are 8 headers in total, which together can represent 256 variables, which is exactly the size of a conflict table.

Figure 7 is a schematic diagram of the formula dividing method of the present disclosure.

In current programmable switches, the TCAM table size is no more than 512 bits wide. Since in the design of this disclosure, the conflict table has two fields of equal length, value and assigned, a conflict table can handle conflicts of up to 256 variables at the same time. In order to handle larger SAT formulas, the present disclosure designs a formula partitioning algorithm, that is, by dividing a large SAT formula data into several small parts, and then putting the small parts into the corresponding conflict table one by one, a programmable switch can be realized Compatibility with large formulas.

The formula partitioning algorithm of the present disclosure divides the entire formula according to the width of the table matching key. It iterates through all clauses of the entire formula and then decides whether to partition the clauses into the current matching table based on whether the table has sufficient capacity. If the table's match-key has sufficient free width and the table is not full, the algorithm divides the clause into the current table. If the match-key of the table has sufficient free width, but the current table is full, the algorithm will not split the clause into tables; and vice versa. Of course, if all the variables contained in a clause are already included in the table, and the table is not full, then the clause will also be included in the table.

As shown in (a) (b) (c) in Figure 7, there are two tables, namely table 1 (table1) and table 2 (table2). Assume that the matching key width of the table is 5 bits and can only contain at most 2 entries. For the first clause, since Table 1 is empty at this time, it can be placed directly into Table 1. For the second clause, it has a variable that is already included in table 1, so if you want to put it into table 1, you need to consume one bit of width on the match-key of table 1. At this time, the match-key of table 1 still has enough free bits, but table 1 is not full, so the second clause can be put into table 1. If you want to put the third clause into Table 1, the situation is the same as the second clause. But now the bit width in table 1 is exhausted and no new variables can be loaded, so the third clause can only be put into table 2.

Figure 8 is a schematic structural diagram of a unit table according to an embodiment of the present disclosure.

As shown in Figure 8, the main function of the unit table is to quickly determine whether unit clause variables are generated. It is similar in principle to a conflict table. A clause generates a unit variable if only one of its variables has been assigned a value and all assigned variables evaluate to false. In this case, the condition for no conflict is that the remaining variables evaluate to true. That is, for a clause with k variables, there are k ways to generate unit variables.

As shown in Figure 8, for a clause with 3 variables, it generates 3 different cell assignments. As with false assignment, when a cell assignment occurs within the current assignment, the current assignment must generate the cell variable throughout the SAT formula. Therefore, the cell table of the cell assignment conversion can perform similar functions to the conflict table. When the cell table is hit, it means that the current assignment must generate cell variables throughout the SAT formula data.

The conflict table returns the result directly and calls the conflict handling function, but the unit table returns an additional parameter indicating which unit variable was generated by the entry. The unit table does not need to consider the priority of the entry. For cell tables, all cell variables generated by the current assignment have the same priority. After the first unit variable is processed, the remaining unit variables are recognized and processed again when entering the unit table later.

Figure 9 is a schematic diagram of the header structure of the search component (SEARCH) according to an embodiment of the present disclosure.

As shown in Figure 9, the search component (SEARCH) header contains fields and their corresponding meanings as follows. IF_CONTINUE and IF_CONFLICT are the return values of the two tables (conflict table and unit table) to record whether there is a conflict; HAVE_DATA is used to determine whether there is currently accompanying formula information in the header; VALUE_TO_SET is used to record whether the variable should be assigned a value of true or not False; FIND_OR_UNIT records whether the currently assigned variable is a unit variable; OP records what the current operation is; IF_OP_DONE records whether the current operation is completed; the three fields TABLE_INDEX, SEGMENT_INDEX, and POSITION_INDEX are used to record the position of the current operation variable in the formula Index; ID_NOW records the id of the current variable; ID_ALL records how many variables there are in the current formula; LAYER records the number of layers of the current search space on the stack; CLAUSE_ID and VARIABLE_ID are operation auxiliary variables, providing storage space for auxiliary variables.

Figure 10 is a schematic diagram of a stack structure according to an embodiment of the present disclosure.

As shown in Figure 10, the get and push operations of the stack are placed on the same stage (actually, due to atomicity restrictions, they can only be placed on the same stage), but the conditions required to execute these two actions are different. of. When the OP is 213, the matching table is hit and the push operation is performed. The acquisition operation cannot be performed at this time. When the OP is 210, the matching table is hit and the get operation is performed. Push operations cannot be performed at this time. If the solver needs to get the data immediately after the push operation, it needs to modify the op field and recycle the packet back to the resolver.

The functions of each part in the search component are relatively independent and handle the input and output of the conflict table and unit table respectively.

Figure 11 is a schematic diagram of the search component workflow according to an embodiment of the present disclosure.

As shown in Figure 11, the search component workflow includes the following steps.

In the first step, the search module (Search Part) searches for unassigned variables, finds x1, assigns x1 to false, pushes the result onto the stack and enters it into the conflict table.

In the second step, since there is no conflict, the go-back module (Go-back Part) inputs the current assignment into the unit table.

In the third step, after entering the unit module (Unit Part), since the unit variables are generated, the processing of the unit variables begins.

In the fourth step, the search module receives the data from the unit module and pushes it onto the stack.

In the fifth step, since the current assignment will cause a formula conflict, the go-back module (Go-back Part) obtains historical data from the stack in the fifth step and returns to the search module to start reassignment.

The disclosed data processing method for the programmable switch to handle the SAT problem can be implemented through the following verification conditions, including algorithm implementation, measurement method experimental platform, data set, and comparison method.

A programmable switch of the present disclosure is implemented on a Barefoot Tofino switch. In addition, another version P Server of the programmable switch of the present disclosure is also implemented. P Server handles the SAT problem through the interaction between the programmable switch and the server by deploying the search unit on the server and only deploying the judgment process on the programmable switch. The server will search for variables first. When judgment is needed, P Server will send the data packet carrying the current assignment information to the programmable switch through DPDK for judgment. In this way, programmable switches and servers interact continuously. Finally, the server will obtain the data processing results of the SAT problem. In order to better evaluate the performance of the programmable switch of the present disclosure, a DPLL algorithm implemented entirely on the server side is designed, called Server.

MathSAT is also implemented based on the DPLL algorithm, but adds many optimizations for special situations; Z3 is designed based on the CDCL algorithm.

In terms of the measurement method experimental platform, P4-DPLL and P Server are implemented through a Barefoot Tofino switch and a server with 2 Intel Xeon Silver 4210R CPUs and 128GB memory. Additionally, a server with 2 Intel Xeon Silver 4210R CPUs and 128GB of memory is used to implement Server.

In terms of data sets, SAT problems are collected from two public data sets, SATLIB-Benchmark Problems and TheInternational SAT Competition. There are a total of 46,787 CNF paradigms in these two datasets, of which 46,685 are satisfiable and 102 are unsatisfiable. Variables in these paradigms range from 20 to 63624, and clauses range from 80 to 368352.

In terms of comparison of similar methods, in order to verify the performance of the programmable switch of the present disclosure, five methods were used for comparison, namely: P4-DPLL, P Server, Server, Z3 and Math SAT. Math SAT and Z3 are the most commonly used algorithms for handling SAT problems and have good performance in current applications. Among them, the solution times of different SAT algorithms were tested and analyzed on the same data set. In order to fairly compare the time consumption of each algorithm, the time consumption here does not include the time spent in preprocessing. In order to analyze the time advantage area between each method, the solution time is further divided into search time and judgment time.

Based on the above verification preparations, the disclosed data processing method was verified from the following aspects: overall performance, performance in solving formulas of different sizes, and time-consuming comparison of judgment time and search time.

Figure 12 is a schematic diagram of performance evaluation results of a programmable switch according to an embodiment of the present disclosure.

Statistics on the solution time of formulas collected from a data set. The CDF is plotted in Figure 12(a) and the 90% quantile of all test cases for each method is given in Figure 12(b). It can be seen that compared with implementing the DPLL algorithm on the CPU, the programmable switch of the present disclosure improves the solution time by 101 times and 16 times respectively on the 90% quantile of all test cases. In addition, it can be seen from (a) in Figure 12 that the processing time of the data processing method of the programmable switch of the present disclosure is faster than Math SAT and Z3 at the 50% quantile of all test cases. The reason why Math SAT and Z3 are faster than P4-DPLL for a large part of the instances is that Z3 uses CDCL, which is inherently much faster than DPLL. Math SAT adopts many instance-related optimizations on DPLL, such as variable elimination, inclusion clauses Remove and reverse include.

In order to analyze the impact of formulas of different sizes on the performance of the SAT solver, the formulas in the dataset were divided into 8 different categories based on the number of variables and the number of clauses. For different types of formulas, the evaluation results of different SAT solvers are analyzed separately. Figure 12(c) shows the solution time for the 90% quantile case for different formula sizes. As the number of variables in the formula increases, the processing time of P Server version SAT solver, Server version SAT solver, and Z3 increases significantly. There is no significant difference between the solution time of MathSAT and the processing time of the programmable switch of the present disclosure. Furthermore, the programmable switch of the present disclosure has significant performance advantages over other solvers when the formula is small. When the formula is relatively large, the performance of the programmable switch of the present disclosure is similar to Math SAT.

For the processing time, it is further divided into search time and judgment time to analyze the time advantage area between each solver.

(d) in Figure 12 shows the judgment time and search time of each method. The disclosed programmable switch solver has the shortest judgment time, and the Server version SAT solver has the longest judgment time. This is because the programmable switch of the present disclosure uses a table of programmable switches for judgment, and can obtain the judgment result in linear time. Although the P Server version of the SAT solver also uses a programmable switch to determine whether assignments conflict, it requires frequent sending and receiving of messages through the server to obtain the switch's determination results. Therefore, the judgment time of the programmable switch of the present disclosure is shorter than that of the P Server version SAT solver. It can be seen that compared with the P Server version SAT solver and the Server version SAT solver, the programmable switch of the present disclosure increases the judgment speed by 246 times and 35 times respectively. In addition, it can be seen that the programmable switch solver of the present disclosure has the largest proportion of decision time. This is because the programmable switch of the present disclosure uses a stack to implement the algorithm, and each check requires multiple calls to the stack. This increases search time and thus reduces decision time.

In summary, it can be seen that the programmable switch (P4-DPLL) of the present disclosure has significant performance improvement compared with the P Server version SAT solver and the Server version SAT solver. Furthermore, P4-DPLL’s SAT solution time is faster than Math SAT and Z3 at the 50% quantile of all test cases. Specifically, P4-DPLL has obvious performance advantages for small formulas. For relatively large formulas, the P4-DPLL solver is comparable to the currently popular Math SAT solver. In addition, the judgment time of P4-DPLL is significantly shorter than that of the PServer version SAT solver and the Server version SAT solver. This is due to the use of tables in the programmable switch to speed up conflict judgment.

In summary, this disclosure implements a SAT parser on Barefoot Tofino switches and commodity servers, and extensively evaluates its performance. The results show that compared to the CPU-based DPLL implementation, the disclosed programmable switch (P4-DPLL) improves processing speed by 101 times at the 90% quantile of all test cases.

In the description of this specification, reference to the description of the terms "one embodiment/mode", "some embodiments/ways", "example", "specific example", or "some examples", etc. is meant to be in conjunction with the description of the embodiment/mode. or examples describe specific features, structures, materials, or characteristics that are included in at least one embodiment/mode or example of this application. In this specification, the schematic expressions of the above terms are not necessarily the same embodiment/mode or example. Furthermore, the specific features, structures, materials or characteristics described may be combined in any suitable manner in any one or more embodiments or examples. Furthermore, those skilled in the art may combine and combine different embodiments/ways or examples and features of different embodiments/ways or examples described in this specification unless they are inconsistent with each other.

In addition, the terms “first” and “second” are used for descriptive purposes only and cannot be understood as indicating or implying relative importance or implicitly indicating the quantity of indicated technical features. Therefore, features defined as "first" and "second" may explicitly or implicitly include at least one of these features. In the description of this application, "plurality" means at least two, such as two, three, etc., unless otherwise expressly and specifically limited.

Those skilled in the art should understand that the above-mentioned embodiments are only for clearly illustrating the present disclosure, but are not intended to limit the scope of the present disclosure. For those skilled in the art, other changes or modifications can be made based on the above disclosure, and these changes or modifications are still within the scope of the present disclosure.

Claims (6)

1. A data processing method for a programmable switch to handle SAT problems, which is characterized by including: The programmable switch receives the SAT formula data preprocessed by the server; the preprocessing includes: dividing the SAT formula data into multiple clauses; the programmable switch receives the SAT formula data preprocessed by the server, including: the programmable switch divides the SAT formula data into multiple clauses. Multiple clauses are placed in different conflict tables; The programmable switch receives the solution instructions sent by the server; the solution instructions are sent in the form of data packets. The data packets include control information for solving SAT. The control information is encapsulated in the form of a packet header. The packet header includes a network type field, Search field and multiple judgment fields, the network type field is used to identify the network type applicable to the SAT solution method; the search field includes control information including assignable variable search, stack operation and unit table matching; and each judgment field Including the information of the conflict table and the conflict processing function, the information of the unit table and the unit processing function; Programmable switches solve SAT problems; and The programmable switch sends the SAT problem solving results to the server; Among them, programmable switches solve SAT problems, including: Search for assignable variables in the SAT formula data and assign values to the variables in the clauses of the SAT formula data; Push the assigned variable onto the stack; Send the variables after assignment to the conflict table, and use the conflict table to determine whether there is a conflict after the variable assignment. If there is a conflict, go back to the stack and reassign the assignable variable. If there is no conflict, proceed to the unit table. matches; and Determine whether to generate unit variables based on the matching results of the unit table. If unit variables are generated, assign values to the unit variables. If no unit variables are generated, search for other assignable variables in the clauses of the SAT formula data. 2. The data processing method according to claim 1, characterized in that determining whether there is a conflict after variable assignment through a conflict table includes: While assigning values to each variable in the clause of the SAT formula data one by one, determine whether each variable in the clause has been assigned a value through the assignment field of the conflict table; When the assignment of each variable in the clause of the SAT formula data has been completed, determine whether the assignment of values to the clause of the SAT formula data causes a conflict; and If a conflict occurs, the conflict is handled through the conflict handling function of the conflict table. 3. The data processing method according to claim 2, characterized in that, judging whether each variable of the clause has been assigned a value through the assignment field of the conflict table, includes: Initialize assigned fields to unassigned status information; After assigning a value to each variable, modify the assignment field corresponding to the variable to the assigned status information; and If the corresponding assignment fields of the clause variables have been modified to the assigned state, it is determined that each variable of the clause has been assigned a value. 4. The data processing method according to claim 1, characterized in that determining whether to generate unit variables includes: When each variable in the clause is assigned until only one variable is left without a value, it is determined that the only remaining variable without a value is a unit variable. 5. The data processing method according to claim 1, characterized in that, backtracking the stack to find assignable variables is performed through a pointer, and the pointer ensures that the variable currently pointed to and the variables directly or indirectly linked to the current variable through the pointer have been Complete assignments to reduce search time for assignable variables. 6. A programmable switch, characterized in that it includes: SAT formula data receiving module, the SAT formula data receiving module is used to receive SAT formula data preprocessed by the server; the preprocessing includes: dividing the SAT formula data into multiple clauses; the SAT formula data receiving module is used to receive the server The preprocessed SAT formula data includes: the SAT formula data receiving module puts the multiple clauses into different conflict tables; Solving instruction processing module, the solving instruction processing module receives the solving instructions sent by the server; the solving instructions are sent in the form of data packets, the data packets include control information for solving SAT, and the control information is encapsulated in the form of a header, The header includes a network type field, a search field and multiple judgment fields. The network type field is used to identify the network type for which the SAT solution method is applicable; the search field includes assignable variable search, stack operation and unit table matching. The control information; and each judgment field includes the information of the conflict table and the conflict processing function, the information of the unit table and the unit processing function; SAT problem solving module, the SAT problem solving module solves SAT problems; and A result sending module, the result sending module is used to send the SAT problem solving results to the server; Among them, the SAT problem solving module includes: A search component used to search for assignable variables and assign values to the variables; and A judgment component that judges whether the assignment will cause conflicts and whether there are unit variables; Wherein, the search component is composed of a stack formed by registers and SRAM, and the search component includes: A search module, which determines assignable variables by traversing all variables, and assigns values to the assignable variables as input to the conflict table; A rollback module that re-searches assignable variables through the backtrace stack based on the conflict table matching results; The unit module, based on the judgment result of the unit table, sends a notification to the search module and assigns values to the unit variables if there are unit variables; Wherein, the judgment component includes a conflict table and a unit table. It is judged based on the conflict table whether the variable assignment to the SAT formula data clause will cause a conflict, and it is judged whether there is a unit variable based on the unit table.