US 11,080,360 B2Granted

Transformation from general max sat to MAX 2SAT

AssigneeInternational Business Machines Corporation

InventorHiroki Yanagisawa

Life of this patent

Estimating the term…

Abstract

A computer-implemented method for solving a MAX SAT instance in provided in which a MAX SAT instance is transformed into a MAX 3SAT instance. The MAX 3SAT instance is transformed into a MAX 2SAT instance which is solved for an optimum solution. A solution to the MAX SAT instance is recovered from the MAX 2SAT optimum solution.

Claims18

Dependent claims

A computer-implemented method for reducing processing time and computational resources used by at least one hardware processor to verify at least one component of a computer system, the method comprising:

verifying, by at least one hardware processor operatively coupled to a computer memory, at least one component of a computer system using an optimum solution o a general MAX SAT instance obtained from optimum solution to a MAX 2SAT instance, the general MAX SAT instance being stored in the computer memory and comprising a set of clauses containing Boolean variables connected by disjunctions, wherein verifying the at least one component of the computer system includes obtaining the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance by:
transforming, by at least one hardware processor, the general MAX SAT instance into a MAX 3SAT instance by converting the clauses in MAX SAT into sets of clauses of at most 3 variables;
transforming, by the at least one hardware processor, the MAX 3SAT instance into the MAX 2SAT instance by converting the clauses in MAX 3SAT into sets of clauses of at most 2 variables, the MAX 2SAT instance;
solving, by the at least one hardware processor, the MAX 2SAT instance by obtaining an optimum solution to the MAX 2SAT instance, including performing an algorithm based on half integrality and persistency properties associated with the MAX 2SAT instance;
and
recovering, by the at least one hardware processor, the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance;
wherein, due at least in part to the performance of the algorithm based on the half integrality and persistency properties, recovering the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance reduces processing time and computational resources used by the at least one hardware processor for verifying the at least one component of the computer system by reducing processing time and computational resources used by the at least one hardware processor for recovering the optimum solution to the general MAX SAT instance when compared to obtaining the optimum solution to the general MAX SAT instance directly from the general MAX SAT instance.

4 more elements

A system comprising:

memory for storing a general MAX SAT instance comprising a set of clauses containing Boolean variables connected by disjunctions;
and
one or more hardware processors operatively coupled to the memory and configured to execute program code implementing a method for reducing processing time and computational resources used by the one or more hardware processors to verify at least one component of a computer system, the method comprising:
verifying the at least one component of a computer system using an optimum solution to the general MAX SAT instance obtained from an optimum solution to a MAX 2SAT instance, including obtaining the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance by:
transforming the general MAX SAT instance into a MAX 3SAT instance by converting the clauses in MAX SAT into sets of clauses of at most 3 variables;
transforming the MAX 3SAT instance into the MAX 2SAT instance by converting the clauses in MAX 3SAT into sets of clauses of at most 2 variables, the MAX 2SAT instance;
solving the MAX 2SAT instance by obtaining an optimum solution to the MAX 2SAT instance, including performing an algorithm based on half integrality and persistency properties associated with the MAX 2SAT instance;
and
recovering the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance;
wherein, due at least in part to the performance of the algorithm based on the half integrality and persistency properties, recovering the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance reduces processing time and computational resources used by the at least one hardware processor for verifying the at least one component of the computer system by reducing processing time and computational resources used by the at least one hardware processor for recovering the optimum solution to the general MAX SAT instance when compared to obtaining the optimum solution to the general MAX SAT instance directly from the general MAX SAT instance.

7 more elements

A computer program product comprising a non-transitory computer readable storage medium having program instructions embodied therewith, the program instructions being executable by a computer to cause the computer to perform a method for reducing processing time and computational resources used by at least one hardware processor to verity at least one component of a computer system the method comprising:

verifying at least one component of a computer system using an optimum solution to a general MAX SAT instance obtained from an optimum solution to a MAX 2SAT instance, the general MAX SAT instance being stored in a computer memory and comprising a set of clauses containing Boolean variables connected by disjunctions, wherein verifying the at least one component of the computer system includes obtaining the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance by:
transforming the general MAX SAT instance into a MAX 3SAT instance by converting the clauses in MAX SAT into sets of clauses of at most 3 variables;
transforming the MAX 3SAT instance into the MAX 2SAT instance by converting the clauses in MAX 3SAT into sets of clauses of at most 2 variables, the MAX 2SAT instance;
solving the MAX 2SAT instance by obtaining an optimum solution to the MAX 2SAT instance, including performing an algorithm based on half integrality and persistency properties associated with the MAX 2SAT instance;
and
recovering an optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance;
wherein, due at least in part to the performance of the algorithm based on the half integrality and persistency properties, recovering the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance reduces processing time and computational resources used by the at least one hardware processor for verifying the at least one component of the computer system by reducing processing time and computational resources used by the at least one hardware processor for recovering the optimum solution to the general MAX SAT instance when compared to obtaining the optimum solution to the general MAX SAT instance directly from the general MAX SAT instance.

4 more elements

Dependencies are inferred from the claim text.

patentgrep

Loading patent…

Abstract

verifying, by at least one hardware processor operatively coupled to a computer memory, at least one component of a computer system using an optimum solution o a general MAX SAT instance obtained from optimum solution to a MAX 2SAT instance, the general MAX SAT instance being stored in the computer memory and comprising a set of clauses containing Boolean variables connected by disjunctions, wherein verifying the at least one component of the computer system includes obtaining the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance by:
transforming, by at least one hardware processor, the general MAX SAT instance into a MAX 3SAT instance by converting the clauses in MAX SAT into sets of clauses of at most 3 variables;
transforming, by the at least one hardware processor, the MAX 3SAT instance into the MAX 2SAT instance by converting the clauses in MAX 3SAT into sets of clauses of at most 2 variables, the MAX 2SAT instance;
solving, by the at least one hardware processor, the MAX 2SAT instance by obtaining an optimum solution to the MAX 2SAT instance, including performing an algorithm based on half integrality and persistency properties associated with the MAX 2SAT instance;
and
recovering, by the at least one hardware processor, the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance;
wherein, due at least in part to the performance of the algorithm based on the half integrality and persistency properties, recovering the optimum solution to the general MAX SAT instance from the optimum solution to the MAX 2SAT instance reduces processing time and computational resources used by the at least one hardware processor for verifying the at least one component of the computer system by reducing processing time and computational resources used by the at least one hardware processor for recovering the optimum solution to the general MAX SAT instance when compared to obtaining the optimum solution to the general MAX SAT instance directly from the general MAX SAT instance.

4 more elements