Simplifying clauses for MAX-SAT

A computer-implemented method comprising:

• obtaining, via a physical input component of a computing device, a plurality of clauses associated with a graph representing a data structure having a plurality of vertices and a plurality of weighted edges connecting the vertices, the graph representing an arrangement of communication devices in a communication network and the graph displayed on a display interface operated by a user;
• storing the plurality of clauses in a clause storage;
• detecting, via a detecting section, (i) whether the plurality of clauses stored in the clause storage include a first clause (a∨b, H) and a second clause (a∨c, H), where a is a first logical variable, b is a second logical variable, c is a third logical variable, and a weight of H signifies a hard clause that must be satisfied by any assignment of values to a plurality of logical variables, (ii) whether any hard clauses in the plurality of clauses other than the first and second clauses include the literal a, and (iii) whether wunit(ā)+wunit(b)≥Xb and wunit(ā)+wunit(c)≥Xc, where wunit(ā) is the weight w1 of a clause (ā, w1) included in the plurality of clauses, wunit(b) is the weight w2 of a clause (b, w2) included in the plurality of clauses, wunit(c) is the weight w3 of a clause (c, w3) included in the plurality of clauses, Xb is the sum of the weights of all clauses in the plurality of clauses stored in the clause storage, other than hard clauses including the literal a, that include at least one of the literals a and b, and Xc is the sum of the weights of all clauses in the plurality of clauses stored in the clause storage, other than hard clauses including the literal a, that include at least one of the literals a and c;
• storing, in a memory, a modified graph having a modified data structure including the plurality of vertices and corresponding clauses having a non-zero weight;
• simplifying, via a clause simplifying section, the plurality of clauses stored in the clause storage using a processor to generate a plurality of simplified clauses, on the basis of the detecting, the simplifying including modifying the plurality of clauses according to the assumption that b=c if the detecting indicates (i) that the plurality of clauses include the first and second clauses, (ii) that no hard clauses in the plurality of clauses stored in the clause storage other than the first and second clauses include the literal a, and (iii) that wunit(ā)+wunit(b)≥Xb and wunit(ā)+wunit(c)≥Xc;
• determining, via an assignment determining section, an optimal assignment of values to a plurality of logical variables associated with the clauses having only the non-zero weight to find a solution to a maximum cut problem of the graph for producing practical results to reduce computations for finding a solution to a maximum satisfiability (MAX-SAT) instance by determining whether each vertex of the plurality of vertices is in a maximum cut subset;
• and
• outputting the plurality of simplified clauses to an output component, the output component configured to load the plurality of simplified clauses to a server through the communication network and configured to display the plurality of simplified clauses to the display interface.

A non-transitory computer readable storage medium having instructions embodied therewith, the instructions executable by a processor to cause the processor to perform operations comprising:

• obtaining, via a physical input component of a computing device, a plurality of clauses associated with a graph representing a data structure having a plurality of vertices and a plurality of weighted edges connecting the vertices, the graph representing an arrangement of communication devices in a communication network and the graph displayed on a display interface operated by a user;
• storing the plurality of clauses in a clause storage;
• detecting, via a detecting section, (i) whether any clauses in the plurality of clauses stored in the clause storage other than a first clause (a∨b, w11), a second clause (ā∨b, w12), a third clause (a∨c, w21), a fourth clause (ā∨c, w22), and a fifth clause (a, w0), where a is a first logical variable, b is a second logical variable, c is a third logical variable, and w11, w12, w21, and w22 are weights, include a literal of the first logical variable a and a non-zero weight and, (ii) whether min(w11,w12)≥w0+max(w21,w22);
• storing, in a memory, a modified graph having a modified data structure including the plurality of vertices and corresponding clauses having a non-zero weight;
• simplifying, via a clause simplifying section, the plurality of clauses stored in the clause storage using a processor to generate a plurality of simplified clauses on the basis of the detecting, the simplifying including modifying the plurality of clauses according to the assumption that a≠b if the detecting indicates (i) that no clauses in the plurality of clauses stored in the clause storage other than the first, second, third, fourth, and fifth clauses include a literal of the first logical variable a and a non-zero weight and (ii) that min(w11,w12)≥w0+max(w21, w22);
• determining, via an assignment determining section, an optimal assignment of values to a plurality of logical variables associated with the clauses having only the non-zero weight to find a solution to a maximum cut problem of the graph for producing practical results to reduce computations for finding a solution to a maximum satisfiability (MAX-SAT) instance by determining whether each vertex of the plurality of vertices is in a maximum cut subset;
• and
• outputting the plurality of simplified clauses to an output component, the output component configured to load the plurality of simplified clauses to a server through the communication network and configured to display the plurality of simplified clauses to the display interface.