From db0e5f28272a4504906cf1bbf17360b550827b5e Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Tue, 1 Feb 2022 01:24:03 -0500 Subject: [PATCH 1/8] added GeneticMaxSatSolver and support for wcnf --- build.gradle | 2 + .../geneticmaxsat/GeneticMaxSatSolver.java | 175 ++++++++++++++++++ .../GeneticMaxSatSolverFactory.java | 27 +++ .../solver/backend/maxsat/MaxSatSolver.java | 71 ++++++- 4 files changed, 269 insertions(+), 6 deletions(-) create mode 100644 src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java create mode 100644 src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java diff --git a/build.gradle b/build.gradle index e59b451a..634886e6 100644 --- a/build.gradle +++ b/build.gradle @@ -49,6 +49,8 @@ dependencies { implementation files("${checkerJar}") implementation group: 'com.google.errorprone', name: 'javac', version: "$errorproneJavacVersion" + implementation 'io.jenetics:jenetics:6.3.0' + implementation 'org.plumelib:options:1.0.5' implementation 'org.plumelib:plume-util:1.5.8' diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java new file mode 100644 index 00000000..765d7cc5 --- /dev/null +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java @@ -0,0 +1,175 @@ +package checkers.inference.solver.backend.geneticmaxsat; + +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.backend.maxsat.MaxSatSolver; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.FileUtils; +import checkers.inference.solver.util.SolverEnvironment; +import io.jenetics.IntegerGene; +import io.jenetics.MeanAlterer; +import io.jenetics.Mutator; +import io.jenetics.Optimize; +import io.jenetics.RouletteWheelSelector; +import io.jenetics.TournamentSelector; +import io.jenetics.engine.Codecs; +import io.jenetics.engine.Engine; +import io.jenetics.engine.EvolutionResult; +import io.jenetics.engine.EvolutionStatistics; +import io.jenetics.util.IntRange; +import org.sat4j.maxsat.WeightedMaxSatDecorator; +import org.sat4j.maxsat.reader.WDimacsReader; +import org.sat4j.pb.IPBSolver; +import org.sat4j.reader.ParseFormatException; +import org.sat4j.specs.ContradictionException; +import org.sat4j.specs.TimeoutException; + +import javax.lang.model.element.AnnotationMirror; +import java.io.ByteArrayInputStream; +import java.io.File; +import java.io.IOException; +import java.io.InputStream; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.Map; + +import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; +import static io.jenetics.engine.Limits.bySteadyFitness; + +public class GeneticMaxSatSolver extends MaxSatSolver { + + private String wcnfFileContent; + + public GeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, + Collection constraints, MaxSatFormatTranslator formatTranslator, + Lattice lattice) { + super(solverEnvironment, slots, constraints, formatTranslator, lattice); + } + + @Override + public Map solve() { + Map superSolutions = super.solve(); // to create initial set of constraints + + List allLines = null; + + try { + allLines = Files.readAllLines(Paths.get("cnfData/wcnfdata.wcnf")); // read from the wcnf file created by super + } catch (IOException ioException) { + ioException.printStackTrace(); + } + + assert allLines != null; + + wcnfFileContent = String.join("\n", allLines.toArray(new String[0])); + + fit(); + + return superSolutions; + } + + private String changeSoftWeights(int newSoftWeights, String wcnfContent, boolean writeToFile){ + int top = 0; + String[] wcnfContentSplit = wcnfContent.split("\n"); + + StringBuilder WCNFModInput = new StringBuilder(); + + for (String line : wcnfContentSplit) { + + String[] trimAndSplit = line.trim().split(" "); + + if (trimAndSplit[0].equals("p")) { + top = Integer.parseInt(trimAndSplit[4]); + } else if (top != 0 && Integer.parseInt(trimAndSplit[0]) < top) { + trimAndSplit[0] = String.valueOf(newSoftWeights); + } + WCNFModInput.append(String.join(" ", trimAndSplit)); + WCNFModInput.append("\n"); + } + + WCNFModInput.setLength(WCNFModInput.length() - 1); // to prevent unwanted character at the end of file + + if (writeToFile){ + File WCNFData = new File(new File("").getAbsolutePath() + "/cnfData"); + FileUtils.writeFile(new File(WCNFData.getAbsolutePath() + "/" + "wcnfdata_modified.wcnf"), WCNFModInput.toString()); + } + + return WCNFModInput.toString(); + } + + private int fitness(final int[] x) { + IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault();; + WDimacsReader reader = new WDimacsReader(new WeightedMaxSatDecorator(solver)); + Map solutions; + int fitness_count = 0; + + String WCNFModInput = changeSoftWeights(x[0], wcnfFileContent, false); + + InputStream stream = new ByteArrayInputStream(WCNFModInput.getBytes(StandardCharsets.UTF_8)); + + try { + solver = (IPBSolver) reader.parseInstance(stream); + } catch (ContradictionException | IOException | ParseFormatException e) { + System.out.println(e); + } + + try { + if (solver.isSatisfiable()){ + solutions = decode(solver.model()); + + List sol = new ArrayList<>(solutions.values()); + + for (AnnotationMirror sol_0 : sol){ + if (sol_0.toString().equals("@universe.qual.Rep")) + { + fitness_count += 1; + } + } + } + else { + System.out.println("UNSAT at " + x[0]); + } + } catch (TimeoutException e) { + e.printStackTrace(); + } + + System.out.println("Rep count: " + fitness_count); + + return fitness_count; + } + + private void fit() { + final Engine engine = Engine + .builder( + this::fitness, + Codecs.ofVector(IntRange.of(0, 700), 1)) + .populationSize(500) + .offspringFraction(0.7) + .survivorsSelector(new RouletteWheelSelector<>()) + .offspringSelector(new TournamentSelector<>()) + .optimize(Optimize.MAXIMUM) + .alterers( + new Mutator<>(0.03), + new MeanAlterer<>(0.6)) + .build(); + + final EvolutionStatistics + statistics = EvolutionStatistics.ofNumber(); + + final EvolutionResult best_res = engine.stream() + .limit(bySteadyFitness(7)) + .limit(100) + .peek(statistics) + .collect(toBestEvolutionResult()); + + System.out.println(statistics); + System.out.println(best_res.genotypes().length()); + System.out.println(best_res.bestPhenotype()); + System.out.println(best_res.worstPhenotype()); + } + +} diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java new file mode 100644 index 00000000..d8cf32a5 --- /dev/null +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java @@ -0,0 +1,27 @@ +package checkers.inference.solver.backend.geneticmaxsat; + +import java.util.Collection; + +import checkers.inference.model.Constraint; +import checkers.inference.model.Slot; +import checkers.inference.solver.backend.AbstractSolverFactory; +import checkers.inference.solver.backend.Solver; +import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; +import checkers.inference.solver.frontend.Lattice; +import checkers.inference.solver.util.SolverEnvironment; + +public class GeneticMaxSatSolverFactory extends AbstractSolverFactory { + + @Override + public Solver createSolver(SolverEnvironment solverEnvironment, Collection slots, + Collection constraints, Lattice lattice) { + MaxSatFormatTranslator formatTranslator = createFormatTranslator(lattice); + return new GeneticMaxSatSolver(solverEnvironment, slots, constraints, formatTranslator, lattice); + } + + @Override + protected MaxSatFormatTranslator createFormatTranslator(Lattice lattice) { + return new MaxSatFormatTranslator(lattice); + } + +} diff --git a/src/checkers/inference/solver/backend/maxsat/MaxSatSolver.java b/src/checkers/inference/solver/backend/maxsat/MaxSatSolver.java index 32430285..f87dca44 100644 --- a/src/checkers/inference/solver/backend/maxsat/MaxSatSolver.java +++ b/src/checkers/inference/solver/backend/maxsat/MaxSatSolver.java @@ -1,6 +1,7 @@ package checkers.inference.solver.backend.maxsat; import java.io.File; +import java.math.BigInteger; import java.util.Collection; import java.util.HashMap; import java.util.HashSet; @@ -20,6 +21,7 @@ import org.sat4j.pb.IPBSolver; import org.sat4j.specs.ContradictionException; import org.sat4j.specs.IConstr; +import org.sat4j.specs.TimeoutException; import org.sat4j.tools.xplain.DeletionStrategy; import org.sat4j.tools.xplain.Xplain; @@ -58,14 +60,16 @@ protected enum MaxSatSolverArg implements SolverArg { private MaxSATUnsatisfiableConstraintExplainer unsatisfiableConstraintExplainer; protected final File CNFData = new File(new File("").getAbsolutePath() + "/cnfData"); protected StringBuilder CNFInput = new StringBuilder(); + protected StringBuilder WCNFInput = new StringBuilder(); + private int sumSoftConstraintWeights = 0; private long serializationStart; private long serializationEnd; protected long solvingStart; protected long solvingEnd; public MaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, - Collection constraints, MaxSatFormatTranslator formatTranslator, Lattice lattice) { + Collection constraints, MaxSatFormatTranslator formatTranslator, Lattice lattice) { super(solverEnvironment, slots, constraints, formatTranslator, lattice); this.slotManager = InferenceMain.getInstance().getSlotManager(); @@ -85,12 +89,15 @@ public Map solve() { this.serializationStart = System.currentTimeMillis(); // Serialization step: encodeAllConstraints(); + solver.setTopWeight(BigInteger.valueOf(sumSoftConstraintWeights + 1)); encodeWellFormednessRestriction(); this.serializationEnd = System.currentTimeMillis(); if (shouldOutputCNF()) { buildCNFInput(); writeCNFInput(); + buildWCNFInput(); + writeWCNFInput(); } // printClauses(); configureSatSolver(solver); @@ -145,7 +152,9 @@ public void encodeAllConstraints() { for (VecInt res : encoding) { if (res != null && res.size() != 0) { if (constraint instanceof PreferenceConstraint) { - softClauses.add(new Pair(res, ((PreferenceConstraint) constraint).getWeight())); + int constraintWeight = ((PreferenceConstraint) constraint).getWeight(); + sumSoftConstraintWeights += constraintWeight; + softClauses.add(new Pair<>(res, constraintWeight)); } else { hardClauses.add(res); } @@ -251,21 +260,71 @@ protected void buildCNFInput() { private void buildCNFInputHelper(VecInt clause) { int[] literals = clause.toArray(); - for (int i = 0; i < literals.length; i++) { - CNFInput.append(literals[i]); + for (int literal : literals) { + CNFInput.append(literal); CNFInput.append(" "); } CNFInput.append("0\n"); } protected void writeCNFInput() { - writeCNFInput("cnfdata.txt"); + writeCNFInput("cnfdata.cnf"); } protected void writeCNFInput(String file) { + CNFInput.setLength(CNFInput.length() - 1); // to prevent unwanted character at the end of file FileUtils.writeFile(new File(CNFData.getAbsolutePath() + "/" + file), CNFInput.toString()); } + /** + * Write WCNF clauses into a string. + */ + protected void buildWCNFInput() { + + final int totalClauses = softClauses.size() + hardClauses.size() + wellFormednessClauses.size(); + final int totalVars = slotManager.getNumberOfSlots() * lattice.numTypes; + final int topWeight = sumSoftConstraintWeights + 1; + + WCNFInput.append("c This is the WCNF input\n"); + WCNFInput.append("p wcnf "); + WCNFInput.append(totalVars); + WCNFInput.append(" "); + WCNFInput.append(totalClauses); + WCNFInput.append(" "); + WCNFInput.append(topWeight); + WCNFInput.append("\n"); + + for (VecInt hardClause : hardClauses) { + buildWCNFInputHelper(hardClause, topWeight); + } + for (VecInt wellFormedNessClause: wellFormednessClauses) { + buildWCNFInputHelper(wellFormedNessClause, topWeight); + } + for (Pair softclause : softClauses) { + buildWCNFInputHelper(softclause.a, softclause.b); + } + } + + private void buildWCNFInputHelper(VecInt clause, int weight) { + int[] literals = clause.toArray(); + WCNFInput.append(weight); + WCNFInput.append(" "); + for (int literal : literals) { + WCNFInput.append(literal); + WCNFInput.append(" "); + } + WCNFInput.append("0\n"); + } + + protected void writeWCNFInput() { + writeWCNFInput("wcnfdata.wcnf"); + } + + protected void writeWCNFInput(String file) { + WCNFInput.setLength(WCNFInput.length() - 1); // to prevent unwanted character at the end of file + FileUtils.writeFile(new File(CNFData.getAbsolutePath() + "/" + file), WCNFInput.toString()); + } + /** * print all soft and hard clauses for testing. */ @@ -370,7 +429,7 @@ public Collection minimumUnsatisfiableConstraints() { } private void configureExplanationSolver(final List hardClauses, final List wellformedness, - final SlotManager slotManager, final Lattice lattice, final Xplain explainer) { + final SlotManager slotManager, final Lattice lattice, final Xplain explainer) { int numberOfNewVars = slotManager.getNumberOfSlots() * lattice.numTypes; System.out.println("Number of variables: " + numberOfNewVars); int numberOfClauses = hardClauses.size() + wellformedness.size(); From e5250031bc76d2ccd14dfa8d54fe616c08a3efa6 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Mon, 7 Feb 2022 10:04:10 -0500 Subject: [PATCH 2/8] added support for multiple Preference Constraints --- .../geneticmaxsat/GeneticMaxSatSolver.java | 145 +++++++----------- 1 file changed, 56 insertions(+), 89 deletions(-) diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java index 765d7cc5..11b0d261 100644 --- a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java @@ -7,43 +7,33 @@ import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.FileUtils; import checkers.inference.solver.util.SolverEnvironment; -import io.jenetics.IntegerGene; -import io.jenetics.MeanAlterer; -import io.jenetics.Mutator; -import io.jenetics.Optimize; -import io.jenetics.RouletteWheelSelector; -import io.jenetics.TournamentSelector; -import io.jenetics.engine.Codecs; -import io.jenetics.engine.Engine; -import io.jenetics.engine.EvolutionResult; -import io.jenetics.engine.EvolutionStatistics; -import io.jenetics.util.IntRange; -import org.sat4j.maxsat.WeightedMaxSatDecorator; -import org.sat4j.maxsat.reader.WDimacsReader; -import org.sat4j.pb.IPBSolver; -import org.sat4j.reader.ParseFormatException; -import org.sat4j.specs.ContradictionException; -import org.sat4j.specs.TimeoutException; +import org.checkerframework.javacutil.BugInCF; +import org.plumelib.util.Pair; +import org.sat4j.core.VecInt; import javax.lang.model.element.AnnotationMirror; -import java.io.ByteArrayInputStream; import java.io.File; import java.io.IOException; -import java.io.InputStream; -import java.nio.charset.StandardCharsets; import java.nio.file.Files; import java.nio.file.Paths; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collection; +import java.util.Collections; +import java.util.HashMap; import java.util.List; import java.util.Map; - -import static io.jenetics.engine.EvolutionResult.toBestEvolutionResult; -import static io.jenetics.engine.Limits.bySteadyFitness; +import java.util.function.Function; +import java.util.stream.Collectors; public class GeneticMaxSatSolver extends MaxSatSolver { - private String wcnfFileContent; + public int allSoftWeightsCount = 0; + public long allSoftWeightsSum = 0; + public List oldSoftWeights; + public List> softWeightsCounter; + public long uniqueSoftWeightsCount = 0; + public String wcnfFileContent; public GeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, Collection constraints, MaxSatFormatTranslator formatTranslator, @@ -67,14 +57,26 @@ public Map solve() { wcnfFileContent = String.join("\n", allLines.toArray(new String[0])); + softWeightCounter(); fit(); return superSolutions; } - private String changeSoftWeights(int newSoftWeights, String wcnfContent, boolean writeToFile){ - int top = 0; - String[] wcnfContentSplit = wcnfContent.split("\n"); + public String changeSoftWeights(int[] newSoftWeights, boolean writeToFile){ + int oldTop = 0; + int currentSoftWeightsSum = 0; + HashMap oldNewWeights = new HashMap<>(); + + for (int i=0; i < softWeightsCounter.size(); i++) { + Pair softWeightPair = softWeightsCounter.get(i); + oldNewWeights.put(softWeightPair.a, newSoftWeights[i]); + softWeightsCounter.remove(softWeightPair); + softWeightsCounter.add(new Pair<>(newSoftWeights[i], softWeightPair.b)); // replacing the old weights with new one (count remains the same) + currentSoftWeightsSum += newSoftWeights[i]*softWeightPair.b; + } + + String[] wcnfContentSplit = this.wcnfFileContent.split("\n"); StringBuilder WCNFModInput = new StringBuilder(); @@ -82,10 +84,13 @@ private String changeSoftWeights(int newSoftWeights, String wcnfContent, boolean String[] trimAndSplit = line.trim().split(" "); + int weight = Integer.parseInt(trimAndSplit[0]); + if (trimAndSplit[0].equals("p")) { - top = Integer.parseInt(trimAndSplit[4]); - } else if (top != 0 && Integer.parseInt(trimAndSplit[0]) < top) { - trimAndSplit[0] = String.valueOf(newSoftWeights); + oldTop = Integer.parseInt(trimAndSplit[4]); + trimAndSplit[4] = String.valueOf(currentSoftWeightsSum); // replacing the top value with current sum of soft weights + } else if (oldTop != 0 && weight < oldTop) { + trimAndSplit[0] = String.valueOf(oldNewWeights.get(weight)); } WCNFModInput.append(String.join(" ", trimAndSplit)); WCNFModInput.append("\n"); @@ -101,75 +106,37 @@ private String changeSoftWeights(int newSoftWeights, String wcnfContent, boolean return WCNFModInput.toString(); } - private int fitness(final int[] x) { - IPBSolver solver = org.sat4j.maxsat.SolverFactory.newDefault();; - WDimacsReader reader = new WDimacsReader(new WeightedMaxSatDecorator(solver)); - Map solutions; - int fitness_count = 0; - - String WCNFModInput = changeSoftWeights(x[0], wcnfFileContent, false); - - InputStream stream = new ByteArrayInputStream(WCNFModInput.getBytes(StandardCharsets.UTF_8)); + public void softWeightCounter(){ - try { - solver = (IPBSolver) reader.parseInstance(stream); - } catch (ContradictionException | IOException | ParseFormatException e) { - System.out.println(e); - } + int top = 0; + List allSoftWeights = new ArrayList<>(); + String[] wcnfContentSplit = this.wcnfFileContent.split("\n"); - try { - if (solver.isSatisfiable()){ - solutions = decode(solver.model()); + for (String line : wcnfContentSplit) { - List sol = new ArrayList<>(solutions.values()); + String[] trimAndSplit = line.trim().split(" "); + int weightValue = Integer.parseInt(trimAndSplit[0]); - for (AnnotationMirror sol_0 : sol){ - if (sol_0.toString().equals("@universe.qual.Rep")) - { - fitness_count += 1; - } - } - } - else { - System.out.println("UNSAT at " + x[0]); + if (trimAndSplit[0].equals("p")) { + top = Integer.parseInt(trimAndSplit[4]); + } else if (top != 0 && weightValue < top) { + allSoftWeights.add(weightValue); } - } catch (TimeoutException e) { - e.printStackTrace(); } - System.out.println("Rep count: " + fitness_count); + allSoftWeightsSum = allSoftWeights.stream().mapToLong(Integer::longValue).sum(); + allSoftWeightsCount = allSoftWeights.size(); + uniqueSoftWeightsCount = allSoftWeights.stream().distinct().count(); + oldSoftWeights = allSoftWeights.stream().distinct().collect(Collectors.toList()); + + for (int weight: oldSoftWeights) { + softWeightsCounter.add(new Pair<>(weight, Collections.frequency(allSoftWeights, weight))); + } - return fitness_count; } - private void fit() { - final Engine engine = Engine - .builder( - this::fitness, - Codecs.ofVector(IntRange.of(0, 700), 1)) - .populationSize(500) - .offspringFraction(0.7) - .survivorsSelector(new RouletteWheelSelector<>()) - .offspringSelector(new TournamentSelector<>()) - .optimize(Optimize.MAXIMUM) - .alterers( - new Mutator<>(0.03), - new MeanAlterer<>(0.6)) - .build(); - - final EvolutionStatistics - statistics = EvolutionStatistics.ofNumber(); - - final EvolutionResult best_res = engine.stream() - .limit(bySteadyFitness(7)) - .limit(100) - .peek(statistics) - .collect(toBestEvolutionResult()); - - System.out.println(statistics); - System.out.println(best_res.genotypes().length()); - System.out.println(best_res.bestPhenotype()); - System.out.println(best_res.worstPhenotype()); + public void fit() { + throw new BugInCF("Method needs to be overridden"); } } From cc4ea04dfafa93d9278048ff1abdbcf064576521 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Mon, 7 Feb 2022 14:45:59 -0500 Subject: [PATCH 3/8] minor fix --- .../geneticmaxsat/GeneticMaxSatSolver.java | 27 ++++++++----------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java index 11b0d261..5f3a3c79 100644 --- a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java @@ -9,7 +9,6 @@ import checkers.inference.solver.util.SolverEnvironment; import org.checkerframework.javacutil.BugInCF; import org.plumelib.util.Pair; -import org.sat4j.core.VecInt; import javax.lang.model.element.AnnotationMirror; import java.io.File; @@ -17,22 +16,21 @@ import java.nio.file.Files; import java.nio.file.Paths; import java.util.ArrayList; -import java.util.Arrays; import java.util.Collection; import java.util.Collections; import java.util.HashMap; +import java.util.LinkedList; import java.util.List; import java.util.Map; -import java.util.function.Function; import java.util.stream.Collectors; public class GeneticMaxSatSolver extends MaxSatSolver { public int allSoftWeightsCount = 0; public long allSoftWeightsSum = 0; - public List oldSoftWeights; - public List> softWeightsCounter; - public long uniqueSoftWeightsCount = 0; + public List oldSoftWeights = new LinkedList<>(); + public List> softWeightsCounter = new LinkedList<>(); + public int uniqueSoftWeightsCount = 0; public String wcnfFileContent; public GeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, @@ -63,7 +61,7 @@ public Map solve() { return superSolutions; } - public String changeSoftWeights(int[] newSoftWeights, boolean writeToFile){ + public String changeSoftWeights(int[] newSoftWeights, List> softWeightsCounter, String wcnfFileContent, boolean writeToFile){ int oldTop = 0; int currentSoftWeightsSum = 0; HashMap oldNewWeights = new HashMap<>(); @@ -76,7 +74,7 @@ public String changeSoftWeights(int[] newSoftWeights, boolean writeToFile){ currentSoftWeightsSum += newSoftWeights[i]*softWeightPair.b; } - String[] wcnfContentSplit = this.wcnfFileContent.split("\n"); + String[] wcnfContentSplit = wcnfFileContent.split("\n"); StringBuilder WCNFModInput = new StringBuilder(); @@ -84,13 +82,11 @@ public String changeSoftWeights(int[] newSoftWeights, boolean writeToFile){ String[] trimAndSplit = line.trim().split(" "); - int weight = Integer.parseInt(trimAndSplit[0]); - if (trimAndSplit[0].equals("p")) { oldTop = Integer.parseInt(trimAndSplit[4]); trimAndSplit[4] = String.valueOf(currentSoftWeightsSum); // replacing the top value with current sum of soft weights - } else if (oldTop != 0 && weight < oldTop) { - trimAndSplit[0] = String.valueOf(oldNewWeights.get(weight)); + } else if (oldTop != 0 && Integer.parseInt(trimAndSplit[0]) < oldTop) { + trimAndSplit[0] = String.valueOf(oldNewWeights.get(Integer.parseInt(trimAndSplit[0]))); } WCNFModInput.append(String.join(" ", trimAndSplit)); WCNFModInput.append("\n"); @@ -115,18 +111,17 @@ public void softWeightCounter(){ for (String line : wcnfContentSplit) { String[] trimAndSplit = line.trim().split(" "); - int weightValue = Integer.parseInt(trimAndSplit[0]); if (trimAndSplit[0].equals("p")) { top = Integer.parseInt(trimAndSplit[4]); - } else if (top != 0 && weightValue < top) { - allSoftWeights.add(weightValue); + } else if (top != 0 && Integer.parseInt(trimAndSplit[0]) < top) { + allSoftWeights.add(Integer.parseInt(trimAndSplit[0])); } } allSoftWeightsSum = allSoftWeights.stream().mapToLong(Integer::longValue).sum(); allSoftWeightsCount = allSoftWeights.size(); - uniqueSoftWeightsCount = allSoftWeights.stream().distinct().count(); + uniqueSoftWeightsCount = (int) allSoftWeights.stream().distinct().count(); oldSoftWeights = allSoftWeights.stream().distinct().collect(Collectors.toList()); for (int weight: oldSoftWeights) { From 8739e088482ee8ab57f421d9eeee3173f353f99a Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Tue, 8 Feb 2022 08:02:22 -0500 Subject: [PATCH 4/8] cleanups --- .../geneticmaxsat/GeneticMaxSatSolver.java | 59 +++++-------------- .../GeneticMaxSatSolverFactory.java | 27 --------- 2 files changed, 14 insertions(+), 72 deletions(-) delete mode 100644 src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java index 5f3a3c79..e69ccc8d 100644 --- a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java @@ -7,30 +7,20 @@ import checkers.inference.solver.frontend.Lattice; import checkers.inference.solver.util.FileUtils; import checkers.inference.solver.util.SolverEnvironment; -import org.checkerframework.javacutil.BugInCF; -import org.plumelib.util.Pair; import javax.lang.model.element.AnnotationMirror; import java.io.File; import java.io.IOException; import java.nio.file.Files; import java.nio.file.Paths; -import java.util.ArrayList; +import java.util.Arrays; import java.util.Collection; -import java.util.Collections; -import java.util.HashMap; -import java.util.LinkedList; import java.util.List; import java.util.Map; -import java.util.stream.Collectors; -public class GeneticMaxSatSolver extends MaxSatSolver { +public abstract class GeneticMaxSatSolver extends MaxSatSolver { public int allSoftWeightsCount = 0; - public long allSoftWeightsSum = 0; - public List oldSoftWeights = new LinkedList<>(); - public List> softWeightsCounter = new LinkedList<>(); - public int uniqueSoftWeightsCount = 0; public String wcnfFileContent; public GeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection slots, @@ -42,7 +32,6 @@ public GeneticMaxSatSolver(SolverEnvironment solverEnvironment, Collection @Override public Map solve() { Map superSolutions = super.solve(); // to create initial set of constraints - List allLines = null; try { @@ -50,9 +39,7 @@ public Map solve() { } catch (IOException ioException) { ioException.printStackTrace(); } - assert allLines != null; - wcnfFileContent = String.join("\n", allLines.toArray(new String[0])); softWeightCounter(); @@ -61,18 +48,9 @@ public Map solve() { return superSolutions; } - public String changeSoftWeights(int[] newSoftWeights, List> softWeightsCounter, String wcnfFileContent, boolean writeToFile){ + public String changeSoftWeights(int[] newSoftWeights, String wcnfFileContent, boolean writeToFile){ int oldTop = 0; - int currentSoftWeightsSum = 0; - HashMap oldNewWeights = new HashMap<>(); - - for (int i=0; i < softWeightsCounter.size(); i++) { - Pair softWeightPair = softWeightsCounter.get(i); - oldNewWeights.put(softWeightPair.a, newSoftWeights[i]); - softWeightsCounter.remove(softWeightPair); - softWeightsCounter.add(new Pair<>(newSoftWeights[i], softWeightPair.b)); // replacing the old weights with new one (count remains the same) - currentSoftWeightsSum += newSoftWeights[i]*softWeightPair.b; - } + int wtIndex = 0; String[] wcnfContentSplit = wcnfFileContent.split("\n"); @@ -84,10 +62,12 @@ public String changeSoftWeights(int[] newSoftWeights, List allSoftWeights = new ArrayList<>(); - String[] wcnfContentSplit = this.wcnfFileContent.split("\n"); + String[] wcnfContentSplit = wcnfFileContent.split("\n"); for (String line : wcnfContentSplit) { String[] trimAndSplit = line.trim().split(" "); + System.out.println(Arrays.toString(trimAndSplit)); + if (trimAndSplit[0].equals("p")) { top = Integer.parseInt(trimAndSplit[4]); } else if (top != 0 && Integer.parseInt(trimAndSplit[0]) < top) { - allSoftWeights.add(Integer.parseInt(trimAndSplit[0])); + allSoftWeightsCount++; } } - - allSoftWeightsSum = allSoftWeights.stream().mapToLong(Integer::longValue).sum(); - allSoftWeightsCount = allSoftWeights.size(); - uniqueSoftWeightsCount = (int) allSoftWeights.stream().distinct().count(); - oldSoftWeights = allSoftWeights.stream().distinct().collect(Collectors.toList()); - - for (int weight: oldSoftWeights) { - softWeightsCounter.add(new Pair<>(weight, Collections.frequency(allSoftWeights, weight))); - } - } - public void fit() { - throw new BugInCF("Method needs to be overridden"); - } + public abstract void fit(); } diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java deleted file mode 100644 index d8cf32a5..00000000 --- a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolverFactory.java +++ /dev/null @@ -1,27 +0,0 @@ -package checkers.inference.solver.backend.geneticmaxsat; - -import java.util.Collection; - -import checkers.inference.model.Constraint; -import checkers.inference.model.Slot; -import checkers.inference.solver.backend.AbstractSolverFactory; -import checkers.inference.solver.backend.Solver; -import checkers.inference.solver.backend.maxsat.MaxSatFormatTranslator; -import checkers.inference.solver.frontend.Lattice; -import checkers.inference.solver.util.SolverEnvironment; - -public class GeneticMaxSatSolverFactory extends AbstractSolverFactory { - - @Override - public Solver createSolver(SolverEnvironment solverEnvironment, Collection slots, - Collection constraints, Lattice lattice) { - MaxSatFormatTranslator formatTranslator = createFormatTranslator(lattice); - return new GeneticMaxSatSolver(solverEnvironment, slots, constraints, formatTranslator, lattice); - } - - @Override - protected MaxSatFormatTranslator createFormatTranslator(Lattice lattice) { - return new MaxSatFormatTranslator(lattice); - } - -} From fdddc5e2e0126313d788d71e6564b9208b15a95e Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Tue, 8 Feb 2022 08:15:16 -0500 Subject: [PATCH 5/8] added comments --- .../solver/backend/geneticmaxsat/GeneticMaxSatSolver.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java index e69ccc8d..2a37ad3a 100644 --- a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java @@ -18,6 +18,10 @@ import java.util.List; import java.util.Map; +/** + * GeneticMaxSatSolver adds support to use Genetic Algorithm to optimize the {@link checkers.inference.model.PreferenceConstraint} weights + * + */ public abstract class GeneticMaxSatSolver extends MaxSatSolver { public int allSoftWeightsCount = 0; @@ -101,6 +105,10 @@ public void softWeightCounter(){ } } + /** + * Override this method to declare an {@link io.jenetics.engine.Engine} builder and create a fitness function. + * For reference, please look at Universe type system. + */ public abstract void fit(); } From b1aa864f5ba46ee7bfe8fdb5d05fd7eec4dae2cf Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Wed, 16 Feb 2022 15:46:50 -0500 Subject: [PATCH 6/8] trying with jenetics 5.2.0 for java8 --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index 634886e6..83610444 100644 --- a/build.gradle +++ b/build.gradle @@ -49,7 +49,7 @@ dependencies { implementation files("${checkerJar}") implementation group: 'com.google.errorprone', name: 'javac', version: "$errorproneJavacVersion" - implementation 'io.jenetics:jenetics:6.3.0' + implementation 'io.jenetics:jenetics:5.2.0' implementation 'org.plumelib:options:1.0.5' implementation 'org.plumelib:plume-util:1.5.8' From 18b3a80e4855f4ef0623d2afe9d92b31be1d8e99 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Wed, 16 Feb 2022 16:03:23 -0500 Subject: [PATCH 7/8] minor print fix --- .../solver/backend/geneticmaxsat/GeneticMaxSatSolver.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java index 2a37ad3a..5c2d4bd3 100644 --- a/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java +++ b/src/checkers/inference/solver/backend/geneticmaxsat/GeneticMaxSatSolver.java @@ -95,8 +95,6 @@ public void softWeightCounter(){ String[] trimAndSplit = line.trim().split(" "); - System.out.println(Arrays.toString(trimAndSplit)); - if (trimAndSplit[0].equals("p")) { top = Integer.parseInt(trimAndSplit[4]); } else if (top != 0 && Integer.parseInt(trimAndSplit[0]) < top) { From fa4d0016f8d9c09a4649713adab505909b654a54 Mon Sep 17 00:00:00 2001 From: Piyush Jha Date: Wed, 16 Feb 2022 16:16:37 -0500 Subject: [PATCH 8/8] jenetics version compatible with java8 and 11 --- build.gradle | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index 83610444..873da930 100644 --- a/build.gradle +++ b/build.gradle @@ -49,7 +49,12 @@ dependencies { implementation files("${checkerJar}") implementation group: 'com.google.errorprone', name: 'javac', version: "$errorproneJavacVersion" - implementation 'io.jenetics:jenetics:5.2.0' + if (isJava8) { + implementation 'io.jenetics:jenetics:5.2.0' + } + else { + implementation 'io.jenetics:jenetics:6.3.0' + } implementation 'org.plumelib:options:1.0.5' implementation 'org.plumelib:plume-util:1.5.8'