Optimal non-recursive method for finding a minimal subset satisfying an upward-closed property

摘要

According to an aspect, a method for providing a minimal explanation to a set of unsatisfiable constraints involves retrieving a minimal subset of constraints that remain together unsatisfiable. The method includes iterating over a list of n constraints, and building a minimal explanation to a set of unsatisfiable constraints by determining which constraint to add to the set of unsatisfiable constraints. Building includes accelerating by removing an increasing number of constraints until removed further constraints makes the set of constraints satisfiable. A dichotomic search is performed on the removed further constraints. The average observed distance is identified between successive constraints in the set of unsatisfiable constraints. A plurality of 2k further constraints located in the list of constraints is removed at the average observed distance from the most recently added constraint. Testing whether a current selected subset is unsatisfiable is performed for the first log2(n) added constraints.

主权项

1. A computer program product for providing a minimal explanation to a set of unsatisfiable constraints, the providing involving retrieving a minimal subset of constraints that remain together unsatisfiable, the computer program product comprising a non-transitory computer readable storage medium having computer readable program code executable by a computer processor to perform:
providing a list of constraints, the list comprising n constraints; and iterating over the list of constraints from a first one of the list of constraints to an nth one of the list of constraints, building a minimal explanation to a set of unsatisfiable constraints by determining which constraint to add to the set of unsatisfiable constraints, the building comprising: identifying an average observed distance between successive constraints in the set of unsatisfiable constraints based on differences in positions of the constraints; if a single removed constraint from the list of constraints keeps the set of constraints unsatisfiable, then starting with k=1, repeating the steps of (a) removing a plurality of 2k further constraints adjacent in the list of constraints to the single removed constraint and (b) incrementing k until the removed plurality of 2k further constraints makes the set of unsatisfiable constraints satisfiable; and if the removed plurality of 2k further constraints makes the set of unsatisfiable constraints satisfiable, returning the most recently removed plurality of 2k further constraints to the set of constraints and removing a subset of one half of the plurality of 2k further constraints, then iteratively removing one half of the remaining constraints in the plurality of 2k further constraints until the set of constraints is satisfiable, then returning the most recently removed constraints.