From 17f3a6cd799bdb5e11884e58cf8d400aec9ef098 Mon Sep 17 00:00:00 2001 From: d367wang <55197967+d367wang@users.noreply.github.com> Date: Wed, 21 Jul 2021 09:38:24 -0400 Subject: [PATCH] Fix MaxSat2TypeSolver (#340) --- .../serialization/CnfVecIntSerializer.java | 48 ++++++++++ .../inference/solver/MaxSat2TypeSolver.java | 90 +++++++++++++------ 2 files changed, 109 insertions(+), 29 deletions(-) diff --git a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java index 63d167692..12feec94a 100644 --- a/src/checkers/inference/model/serialization/CnfVecIntSerializer.java +++ b/src/checkers/inference/model/serialization/CnfVecIntSerializer.java @@ -8,6 +8,7 @@ import checkers.inference.model.LubVariableSlot; import checkers.inference.model.ImplicationConstraint; import checkers.inference.model.VariableSlot; +import org.checkerframework.javacutil.BugInCF; import org.sat4j.core.VecInt; import checkers.inference.SlotManager; @@ -288,12 +289,37 @@ public VecInt[] serialize(ImplicationConstraint implicationConstraint) { "MaxSAT backend. Use MaxSATSolver instead!"); } + /** + * Convert all the given mandatory constraints into hard clauses. A BugInCF exception is + * raised if the given constraints contain any {@link PreferenceConstraint}. + * + * For conversion of constraints containing {@link PreferenceConstraint}, use + * {@link CnfVecIntSerializer#convertAll(Iterable, List, List)} + * + * @param constraints the constraints to convert + * @return the output clauses for the given constraints + */ public List convertAll(Iterable constraints) { return convertAll(constraints, new LinkedList()); } + /** + * Convert all the given mandatory constraints into hard clauses. A BugInCF exception is + * raised if the given constraints contains any {@link PreferenceConstraint}. + * + * For conversion of constraints containing {@link PreferenceConstraint}, use + * {@link CnfVecIntSerializer#convertAll(Iterable, List, List)} + * + * @param constraints the constraints to convert + * @param results the output clauses for the given constraints + * @return same as {@code results} + */ public List convertAll(Iterable constraints, List results) { for (Constraint constraint : constraints) { + if (constraint instanceof PreferenceConstraint) { + throw new BugInCF("CnfVecIntSerializer: adding PreferenceConstraint ( " + constraint + + " ) to hard clauses is forbidden"); + } for (VecInt res : constraint.serialize(this)) { if (res.size() != 0) { results.add(res); @@ -304,6 +330,28 @@ public List convertAll(Iterable constraints, List re return results; } + /** + * Convert all the given mandatory constraints to hard clauses, and preference constraints + * to soft clauses. + * + * @param constraints the constraints to convert + * @param hardClauses the output hard clauses for the mandatory constraints + * @param softClauses the output soft clauses for {@link PreferenceConstraint} + */ + public void convertAll(Iterable constraints, List hardClauses, List softClauses) { + for (Constraint constraint : constraints) { + for (VecInt res : constraint.serialize(this)) { + if (res.size() != 0) { + if (constraint instanceof PreferenceConstraint) { + softClauses.add(res); + } else { + hardClauses.add(res); + } + } + } + } + } + protected abstract boolean isTop(ConstantSlot constantSlot); VecInt asVec(int ... vars) { diff --git a/src/checkers/inference/solver/MaxSat2TypeSolver.java b/src/checkers/inference/solver/MaxSat2TypeSolver.java index bb5779181..d1558afa8 100644 --- a/src/checkers/inference/solver/MaxSat2TypeSolver.java +++ b/src/checkers/inference/solver/MaxSat2TypeSolver.java @@ -7,6 +7,8 @@ import java.util.Collection; import java.util.HashMap; +import java.util.HashSet; +import java.util.LinkedList; import java.util.List; import java.util.Map; @@ -23,6 +25,8 @@ import checkers.inference.model.Constraint; import checkers.inference.model.Slot; import checkers.inference.model.serialization.CnfVecIntSerializer; +import org.sat4j.specs.ContradictionException; +import org.sat4j.specs.TimeoutException; /** * This solver is used to convert any constraint set using a type system with only 2 types (Top/Bottom), @@ -69,9 +73,10 @@ protected boolean isTop(ConstantSlot constantSlot) { } public InferenceResult solve() { - final Map solutions = new HashMap<>(); - final List clauses = serializer.convertAll(constraints); + final List softClauses = new LinkedList<>(); + final List hardClauses = new LinkedList<>(); + serializer.convertAll(constraints, hardClauses, softClauses); // nextId describes the LARGEST id that might be found in a variable // if an exception occurs while creating a variable the id might be incremented @@ -82,7 +87,7 @@ public InferenceResult solve() { // TODO: thus here the value of totalVars is the real slots number stored in slotManager, and plus the // TODO: "fake" slots number stored in existentialToPotentialVar final int totalVars = slotManager.getNumberOfSlots() + serializer.getExistentialToPotentialVar().size(); - final int totalClauses = clauses.size(); + final int totalClauses = hardClauses.size() + softClauses.size(); // When .newBoth is called, SAT4J will run two solvers and return the result of the first to halt @@ -96,42 +101,69 @@ public InferenceResult solve() { VecInt lastClause = null; try { - for (VecInt clause : clauses) { + for (VecInt clause : hardClauses) { + lastClause = clause; + solver.addHardClause(clause); + } + for (VecInt clause : softClauses) { lastClause = clause; solver.addSoftClause(clause); } - // isSatisfiable launches the solvers and waits until one of them finishes - if (solver.isSatisfiable()) { - final Map existentialToPotentialIds = serializer.getExistentialToPotentialVar(); - int[] solution = solver.model(); - - for (Integer var : solution) { - boolean isTop = var < 0; - if (isTop) { - var = -var; - } - - Integer potential = existentialToPotentialIds.get(var); - if (potential != null) { - // idToExistence.put(potential, !isTop); - // TODO: which AnnotationMirror should be used? - solutions.put(potential, bottom); - } else { - solutions.put(var, isTop ? top : bottom ); - } + } catch (ContradictionException ce) { + // This happens when adding a clause causes trivial contradiction, such as adding -1 to {1} + System.out.println("Not solvable! Contradiction exception " + + "when adding clause: " + lastClause + "."); + + // pass empty set as the unsat explanation + // TODO: explain UNSAT possibly by reusing MaxSatSolver.MaxSATUnsatisfiableConstraintExplainer + return new DefaultInferenceResult(new HashSet<>()); + } + boolean isSatisfiable; + try { + // isSatisfiable() launches the solvers and waits until one of them finishes + isSatisfiable = solver.isSatisfiable(); + + } catch(TimeoutException te) { + throw new RuntimeException("MAX-SAT solving timeout! "); + } + + if (!isSatisfiable) { + System.out.println("Not solvable!"); + // pass empty set as the unsat explanation + // TODO: explain UNSAT possibly by reusing MaxSatSolver.MaxSATUnsatisfiableConstraintExplainer + return new DefaultInferenceResult(new HashSet<>()); + } + + int[] solution = solver.model(); + // The following code decodes VecInt solution to the slot-annotation mappings + final Map decodedSolution = new HashMap<>(); + final Map existentialToPotentialIds = serializer.getExistentialToPotentialVar(); + + for (Integer var : solution) { + Integer potential = existentialToPotentialIds.get(Math.abs(var)); + if (potential != null) { + // Assume the 'solution' output by the solver is already sorted in the ascending order + // of their absolute values. So the existential variables come after the potential variables, + // which means the potential slot corresponding to the current existential variable is + // already inserted into 'solutions' + assert decodedSolution.containsKey(potential); + if (var < 0) { + // The existential variable is false, so the potential variable should not be inserted. + // Remove it from the solution. + decodedSolution.remove(potential); } } else { - System.out.println("Not solvable!"); + boolean isTop = var < 0; + if (isTop) { + var = -var; + } + decodedSolution.put(var, isTop ? top : bottom); } - - } catch(Throwable th) { - throw new RuntimeException("Error MAX-SAT solving! " + lastClause, th); } - - return new DefaultInferenceResult(solutions); + return new DefaultInferenceResult(decodedSolution); } }