Explaining illegal combinations in combinatorial models

A computerized apparatus having a processor, the processor being adapted to perform the steps of:

• 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 on a satisfiability formula that encodes the legal test space and that assigns values to attributes as defined by the illegal combination, whereby the satisfiability solver provides an indication of unsatisfiability of the satisfiability 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.

A computer program product comprising:

• a non-transitory computer readable medium retaining program instructions, which instructions when read by a processor, cause the processor to perform a 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 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.