TheorySolver { public static <Constraint, Model> Pair<Model, Collection<Constraint>> solve( Theory<Constraint, Model> theorySolver, FixingSetFinder<Constraint> fixingSetFinder, List<Constraint> hardConstraints, List<Constraint> softConstraints) { FixingSetListener<Constraint, Model> listener = NOISY ? loggingListener() : FixingSetListener.dummyListener(); fixingSetFinder.setup(softConstraints); Collection<Constraint> fixingSet = new ArrayList<>(); Collection<Constraint> positive = new LinkedHashSet<>(); for (;;) { if (Thread.currentThread().isInterrupted()) { throw new RuntimeException("thread was interrupted"); } positive.addAll(hardConstraints); positive.addAll(softConstraints); positive.removeAll(fixingSet); Either<Model, Collection<Constraint>> result = timed(() -> theorySolver.check(positive), "CHECKING THEORY"); if (result.right == null) { if (NOISY) System.out.println("VALID MODEL"); listener.onFixingSet(result.left, fixingSet); return Pair.of(result.left, fixingSet); } else { listener.onCore(result.right); Collection<Constraint> softCore = result.right.stream() .filter(c -> !hardConstraints.contains(c)) .collect(Collectors.toList()); if (softCore.isEmpty()) { throw new IllegalStateException("Hard clauses are unsat!"); } fixingSet.clear(); fixingSetFinder.addCore(softCore); timed(() -> fixingSetFinder.currentFixingSet(fixingSet, listener), "FINDING FIXING SET"); System.out.println(" --> PROPOSAL SIZE = " + fixingSet.size()); } } }  static void enumerateFixingSets(
            FixingSetFinder<Constraint> fixingSetFinder,
            Theory<Constraint, Model> theorySolver,
            Collection<Constraint> hardConstraints,
            Collection<Constraint> softConstraints,
            FixingSetListener<Constraint, Model> listener); static Pair<Model, Collection<Constraint>> solve(
            Theory<Constraint, Model> theorySolver,
            FixingSetFinder<Constraint> fixingSetFinder,
            List<Constraint> hardConstraints,
            List<Constraint> softConstraints); static Pair<Model, Collection<Constraint>> minimizeFixingSet(
        Theory<Constraint, Model> theorySolver,
        List<Constraint> hardConstraints,
        List<Constraint> softConstraints,
        Model model,
        Collection<Constraint> fixingSet);  }
@Test public void testBasics() { List<Object> all = Arrays.asList("a", "b", "c", "d", "e", "f", "g", "h"); for (int i = 0; i < 100; ++i) { Random r = new Random(SEED + i); Collection<Object> truthy = all.stream() .filter(x -> r.nextBoolean()) .collect(Collectors.toSet()); Theory<Object, Void> theory = positive -> { Collection<Object> bad = positive.stream() .filter(x -> !truthy.contains(x)) .collect(Collectors.toSet()); if (bad.size() > 0) { Collection<Object> unsat = new HashSet<>(); unsat.add(bad.iterator().next()); bad.stream().filter(x -> r.nextBoolean()).forEach(unsat::add); return Either.right(unsat); } else { return Either.left(null); } }; Pair<Void, Collection<Object>> result = TheorySolver.solve( theory, new SatFixingSetFinder<>(new Sat4J()), Collections.emptyList(), all); Assert.assertEquals(all.size() - truthy.size(), result.getRight().size()); Assert.assertEquals(truthy, all.stream().filter(x -> !result.getRight().contains(x)).collect(Collectors.toSet())); } }