Searching for Autarkies to Trim Unsatisfiable Clause Sets

摘要: An autarky is a partial assignment to the variables of Boolean CNF formula that satisfies every clause containing an assigned variable. For unsatisfiable formula, provides information about those clauses are essentially independent from infeasibility; satisfied by not contained in any minimal subset (MUS) or correction (MCS) clauses. This suggests preprocessing step detecting autarkies and trimming such instance prior running algorithm for finding MUSes MCSes. With little existing work on algorithms experimental evaluations thereof, there room further research this area. Here, we present novel searches directly using standard satisfiability solver. We investigate several industrial benchmark suites, results show our compares favorably approach discovering autarkies. Finally, explore potential MCS- MUS-extraction flows.