Simplifying clauses for max-sat

A computer-implemented method comprising:

• obtaining a plurality of clauses associated with a plurality of logical variables, each of the clauses including of a weight and a disjunction of one or more literals of the variables;
• detecting (i) whether the plurality of clauses includes a first clause (ab, H) and a second clause (ac, 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 the plurality of logical variables, (ii) whether any hard clauses in the plurality of clause 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 (a, 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, 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, other than hard clauses including the literal a, that include at least one of the literals a and c;
• and
• simplifying the plurality of clauses using a processor, 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 includes the first and second clauses, (ii) that no hard clauses in the plurality of clauses other than the first and second clauses include the literal a, and (iii) that wunit(ā)+wunit(b)≧Xb and wunit(ā)+wunit(c)≧Xc.

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 a plurality of clauses associated with a plurality of logical variables, each of the clauses including of a weight and a disjunction of one or more literals of the logical variables;
• detecting (i) whether any clauses in the plurality of clauses other than a first clause (ab, w11), a second clause (āb, w12), a third clause (ac, 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);
• and
• simplifying the plurality of clauses using a processor 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 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).