Patent ID: 8914757
Filing Date: 2014-12-16
Classification: G06F

Abstract:
1. A computer-implemented method comprising: obtaining a combinatorial model, in a system under test (SUT), defining a legal test space, the combinatorial model comprising a set of attributes, a respective domain for each attribute defining possible values for the attribute, and a set of restrictions, wherein the restrictions define a combination of values of the attributes that are illegal and are excluded from the legal test case; obtaining an illegal combination, wherein the illegal combination is excluded by one or more restrictions; utilizing a Satisfiability solver, executed by a processor, on a satisfiability formula that encodes the legal test space and that assigns values to attributes as defined by the illegal combination, whereby the satistiability solver provides an indication of unsatisfiability of the satistiability formula and an UNSAT core comprising a subset of clauses defined by the satisfiability formula which are unsatisfiable; and identifying the one or more restrictions by mapping the clauses of the UNSAT core with clauses encoding the set of restrictions.