diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/AnswerSet.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/AnswerSet.java index d5b63f74e..27a76a15b 100644 --- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/AnswerSet.java +++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/AnswerSet.java @@ -1,12 +1,13 @@ package at.ac.tuwien.kr.alpha.api; -import java.util.List; -import java.util.SortedSet; - import at.ac.tuwien.kr.alpha.api.programs.Predicate; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.atoms.AtomQuery; +import java.util.List; +import java.util.Map; +import java.util.SortedSet; + /** * API representation of an answer set, i.e. a set of atoms that is a model of an ASP program. * @@ -24,6 +25,11 @@ public interface AnswerSet extends Comparable { */ SortedSet getPredicateInstances(Predicate predicate); + /** + * Returns a mapping of {@link Predicate}s to all respective instances. + */ + Map> getPredicateInstances(); + /** * Boolean flag indicating whether this {@link AnswerSet} represents the empty set. */ diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/Solver.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/Solver.java index 2dbd6be90..6400ea4f5 100644 --- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/Solver.java +++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/Solver.java @@ -38,4 +38,12 @@ default List collectList() { return stream().collect(Collectors.toList()); } + /** + * Reports whether this {@link Solver} completely searched all of the given search space for desired answer sets. + * For this to be true, the solver does not need to check every candidate explicitly, but also use learned knowledge or other + * factors (like optimality) in order to prove that no relevant answer set remains un-investigated. + * @return true iff the given search space was investigated exhaustively. + */ + boolean didExhaustSearchSpace(); + } diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java index 27019ce10..b5af052de 100644 --- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java +++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/config/SystemConfig.java @@ -36,7 +36,7 @@ /** * Config structure for {@link Alpha} instances. - * + * * Copyright (c) 2021, the Alpha Team. */ public class SystemConfig { @@ -64,6 +64,8 @@ public class SystemConfig { public static final boolean DEFAULT_GROUNDER_ACCUMULATOR_ENABLED = false; public static final String DEFAULT_ATOM_SEPARATOR = ", "; public static final AggregateRewritingConfig DEFAULT_AGGREGATE_REWRITING_CONFIG = new AggregateRewritingConfig(); + public static final boolean DEFAULT_OPTIMIZATION_ENABLED = false; + public static final String DEFAULT_MAX_WEIGHT_AT_LEVELS = ""; private String grounderName = DEFAULT_GROUNDER_NAME; private String solverName = DEFAULT_SOLVER_NAME; @@ -85,6 +87,8 @@ public class SystemConfig { private boolean grounderAccumulatorEnabled = DEFAULT_GROUNDER_ACCUMULATOR_ENABLED; private String atomSeparator = DEFAULT_ATOM_SEPARATOR; private AggregateRewritingConfig aggregateRewritingConfig = DEFAULT_AGGREGATE_REWRITING_CONFIG; + private boolean answerSetOptimizationEnabled = DEFAULT_OPTIMIZATION_ENABLED; + private String answerSetsMaxWeightAtLevels = DEFAULT_MAX_WEIGHT_AT_LEVELS; public String getGrounderName() { return this.grounderName; @@ -280,4 +284,19 @@ public void setAggregateRewritingConfig(AggregateRewritingConfig aggregateRewrit this.aggregateRewritingConfig = aggregateRewritingConfig; } + public boolean isAnswerSetOptimizationEnabled() { + return answerSetOptimizationEnabled; + } + + public void setAnswerSetOptimizationEnabled(boolean answerSetOptimizationEnabled) { + this.answerSetOptimizationEnabled = answerSetOptimizationEnabled; + } + + public String getAnswerSetsMaxWeightAtLevels() { + return answerSetsMaxWeightAtLevels; + } + + public void setAnswerSetsMaxWeightAtLevels(String answerSetsMaxWeightAtLevels) { + this.answerSetsMaxWeightAtLevels = answerSetsMaxWeightAtLevels; + } } diff --git a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/Program.java b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/Program.java index eeb251945..6db540a45 100644 --- a/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/Program.java +++ b/alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/programs/Program.java @@ -1,11 +1,11 @@ package at.ac.tuwien.kr.alpha.api.programs; -import java.util.List; - import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.rules.Rule; import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head; +import java.util.List; + /** * An ASP program as accepted by Alpha. * @@ -29,4 +29,10 @@ public interface Program> { */ List getRules(); + /** + * Indicates whether this program contains some weak constraints. + * @return true iff this program contains weak constraints. + */ + boolean containsWeakConstraints(); + } diff --git a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/Main.java b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/Main.java index 46c992573..a073a9af5 100644 --- a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/Main.java +++ b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/Main.java @@ -27,22 +27,6 @@ */ package at.ac.tuwien.kr.alpha; -import java.io.File; -import java.io.FileNotFoundException; -import java.io.FileOutputStream; -import java.io.IOException; -import java.io.PrintStream; -import java.nio.file.Paths; -import java.util.Set; -import java.util.concurrent.atomic.AtomicInteger; -import java.util.function.BiConsumer; -import java.util.stream.Collectors; -import java.util.stream.Stream; - -import org.apache.commons.cli.ParseException; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - import at.ac.tuwien.kr.alpha.api.Alpha; import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.DebugSolvingContext; @@ -61,7 +45,23 @@ import at.ac.tuwien.kr.alpha.app.ComponentGraphWriter; import at.ac.tuwien.kr.alpha.app.DependencyGraphWriter; import at.ac.tuwien.kr.alpha.app.config.CommandLineParser; +import at.ac.tuwien.kr.alpha.commons.WeightedAnswerSet; import at.ac.tuwien.kr.alpha.commons.util.SimpleAnswerSetFormatter; +import org.apache.commons.cli.ParseException; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.io.File; +import java.io.FileNotFoundException; +import java.io.FileOutputStream; +import java.io.IOException; +import java.io.PrintStream; +import java.nio.file.Paths; +import java.util.Set; +import java.util.concurrent.atomic.AtomicInteger; +import java.util.function.BiConsumer; +import java.util.stream.Collectors; +import java.util.stream.Stream; /** * Main entry point for Alpha. @@ -150,7 +150,7 @@ private static void writeComponentGraph(ComponentGraph cg, String path) { } /** - * Writes the given {@link CompiledProgram} to the destination passed as the second parameter + * Writes the given {@link NormalProgram} to the destination passed as the second parameter * * @param prg the program to write * @param path the path to write the program to @@ -186,6 +186,10 @@ private static void computeAndConsumeAnswerSets(Solver solver, AlphaConfig alpha final AnswerSetFormatter fmt = new SimpleAnswerSetFormatter(sysCfg.getAtomSeparator()); BiConsumer stdoutPrinter = (n, as) -> { System.out.println("Answer set " + Integer.toString(n) + ":" + System.lineSeparator() + fmt.format(as)); + if (as instanceof WeightedAnswerSet) { + // If weak constraints are presents, all answer sets are weighted. + System.out.println("Optimization: " + ((WeightedAnswerSet) as).getWeightsAsString()); + } }; if (inputCfg.isWriteAnswerSetsAsXlsx()) { BiConsumer xlsxWriter = new AnswerSetToXlsxWriter(inputCfg.getAnswerSetFileOutputPath()); @@ -208,6 +212,10 @@ private static void computeAndConsumeAnswerSets(Solver solver, AlphaConfig alpha } } else { System.out.println("SATISFIABLE"); + if (sysCfg.isAnswerSetOptimizationEnabled() && solver.didExhaustSearchSpace()) { + // If less answer sets were found than requested and optimisation is enabled, then the last one is an optimal answer set. + System.out.println("OPTIMUM PROVEN"); + } } } else { // Note: Even though we are not consuming the result, we will still compute diff --git a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java index fcefe55fc..dc15a8017 100644 --- a/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java +++ b/alpha-cli-app/src/main/java/at/ac/tuwien/kr/alpha/app/config/CommandLineParser.java @@ -150,6 +150,11 @@ public class CommandLineParser { .desc("a character (sequence) to use as separator for atoms in printed answer sets (default: " + SystemConfig.DEFAULT_ATOM_SEPARATOR + ")") .build(); + private static final Option OPT_ENABLE_OPTIMIZATION = Option.builder("opt").longOpt("enableOptimization") + .desc("enables branch-and-bound answer-set optimization based on the weak constraints of the input program.").build(); + private static final Option OPT_MAXWEIGHT = Option.builder("mw").longOpt("maxWeight").hasArg(true).argName("weight") + .desc("the (weak constraints) valuation of answer sets must be below this weight, only has an effect if answer-set optimization is enabled. " + + "Weights are given as a comma-separated list of weight@level pairs, e.g.: 3@1,2@2,5@-1").build(); //@formatter:on private static final Options CLI_OPTS = new Options(); @@ -191,6 +196,8 @@ public class CommandLineParser { CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED); CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_OUTPUT_ATOM_SEPARATOR); + CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_ENABLE_OPTIMIZATION); + CommandLineParser.CLI_OPTS.addOption(CommandLineParser.OPT_MAXWEIGHT); } /* @@ -248,6 +255,8 @@ private void initializeGlobalOptionHandlers() { this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_TOLERANCE_RULES.getOpt(), this::handleGrounderToleranceRules); this.globalOptionHandlers.put(CommandLineParser.OPT_GROUNDER_ACCUMULATOR_ENABLED.getOpt(), this::handleGrounderNoInstanceRemoval); this.globalOptionHandlers.put(CommandLineParser.OPT_OUTPUT_ATOM_SEPARATOR.getOpt(), this::handleAtomSeparator); + this.globalOptionHandlers.put(CommandLineParser.OPT_ENABLE_OPTIMIZATION.getOpt(), this::handleEnableOptimization); + this.globalOptionHandlers.put(CommandLineParser.OPT_MAXWEIGHT.getOpt(), this::handleMaxWeight); } private void initializeInputOptionHandlers() { @@ -478,4 +487,11 @@ private void handleAtomSeparator(Option opt, SystemConfig cfg) { cfg.setAtomSeparator(StringEscapeUtils.unescapeJava(opt.getValue(SystemConfig.DEFAULT_ATOM_SEPARATOR))); } + private void handleEnableOptimization(Option opt, SystemConfig cfg) { + cfg.setAnswerSetOptimizationEnabled(true); + } + + private void handleMaxWeight(Option opt, SystemConfig cfg) { + cfg.setAnswerSetsMaxWeightAtLevels(opt.getValue(SystemConfig.DEFAULT_MAX_WEIGHT_AT_LEVELS)); + } } diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/BasicAnswerSet.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/BasicAnswerSet.java index c7b006de5..59a3cb1dc 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/BasicAnswerSet.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/BasicAnswerSet.java @@ -1,25 +1,26 @@ package at.ac.tuwien.kr.alpha.commons; -import static java.util.Collections.emptyMap; -import static java.util.Collections.emptySortedSet; +import at.ac.tuwien.kr.alpha.api.AnswerSet; +import at.ac.tuwien.kr.alpha.api.programs.Predicate; +import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.api.programs.atoms.AtomQuery; +import at.ac.tuwien.kr.alpha.commons.util.Util; +import java.util.Collections; import java.util.Iterator; import java.util.List; import java.util.Map; import java.util.Set; import java.util.SortedSet; -import at.ac.tuwien.kr.alpha.api.AnswerSet; -import at.ac.tuwien.kr.alpha.api.programs.Predicate; -import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; -import at.ac.tuwien.kr.alpha.api.programs.atoms.AtomQuery; -import at.ac.tuwien.kr.alpha.commons.util.Util; +import static java.util.Collections.emptyMap; +import static java.util.Collections.emptySortedSet; /** * Copyright (c) 2016, the Alpha Team. */ class BasicAnswerSet implements AnswerSet { - + static final BasicAnswerSet EMPTY = new BasicAnswerSet(emptySortedSet(), emptyMap()); private final SortedSet predicates; @@ -45,6 +46,11 @@ public boolean isEmpty() { return predicates.isEmpty(); } + @Override + public Map> getPredicateInstances() { + return Collections.unmodifiableMap(predicateInstances); + } + @Override public String toString() { if (predicates.isEmpty()) { @@ -101,6 +107,9 @@ public int hashCode() { @Override public int compareTo(AnswerSet other) { + if (other.getClass() != this.getClass()) { + return 1; + } final SortedSet predicates = this.getPredicates(); int result = Util.compareSortedSets(predicates, other.getPredicates()); diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/WeightedAnswerSet.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/WeightedAnswerSet.java new file mode 100644 index 000000000..9720f1f54 --- /dev/null +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/WeightedAnswerSet.java @@ -0,0 +1,154 @@ +package at.ac.tuwien.kr.alpha.commons; + +import at.ac.tuwien.kr.alpha.api.AnswerSet; + +import java.util.Iterator; +import java.util.Map; +import java.util.Objects; +import java.util.StringJoiner; +import java.util.TreeMap; + +/** + * Represents a weighted answer set, i.e., it extends a {@link BasicAnswerSet} with weights information. + * + * Weights are given as a mapping from levels to the respective weight. Note that negative levels and weights are allowed. + * The highest level is the most important one and levels not contained in the map have a weight of zero. + * + * Copyright (c) 2020-2021, the Alpha Team. + */ +public class WeightedAnswerSet extends BasicAnswerSet { + + private final TreeMap weightPerLevel; + + public WeightedAnswerSet(AnswerSet answerSet, TreeMap weightPerLevel) { + super(answerSet.getPredicates(), answerSet.getPredicateInstances()); + this.weightPerLevel = weightPerLevel; + } + + /** + * Compares the weights of this {@link WeightedAnswerSet} with the weights of the other one. + * @param other the {@link WeightedAnswerSet} to compare with. + * @return -1, 0, or 1 depending on whether the weights of this are better, equal, or worse than the other. + */ + public int compareWeights(WeightedAnswerSet other) { + Iterator thisDescIterator = this.weightPerLevel.descendingKeySet().iterator(); + Iterator otherDescIterator = other.weightPerLevel.descendingKeySet().iterator(); + while (true) { + // Descend this level down to one with non-zero weight. + Integer thisLevel = null; + Integer thisWeight = null; + while (thisDescIterator.hasNext()) { + thisLevel = thisDescIterator.next(); + thisWeight = this.weightPerLevel.get(thisLevel); + if (thisWeight != null && thisWeight != 0) { + break; + } + } + // Descend other level down to one with non-zero weight. + Integer otherLevel = null; + Integer otherWeight = null; + while (otherDescIterator.hasNext()) { + otherLevel = otherDescIterator.next(); + otherWeight = other.weightPerLevel.get(otherLevel); + if (otherWeight != null && otherWeight != 0) { + break; + } + } + if (thisWeight == null && otherWeight == null) { + return 0; + } + if (thisWeight == null) { + return otherWeight < 0 ? 1 : -1; + } + if (otherWeight == null) { + return thisWeight < 0 ? -1 : 1; + } + // Found level and weight for this and other WeightedAnswerSet. + if (!thisLevel.equals(otherLevel)) { + return thisLevel < otherLevel ? -1 : 1; + } + if (!thisWeight.equals(otherWeight)) { + return thisWeight < otherWeight ? -1 : 1; + } + // Same level and same weight for both WeightedAnswerSet, now continue with next lower level. + } + } + + @Override + public int compareTo(AnswerSet other) { + if (!(other instanceof WeightedAnswerSet)) { + return -1; + } + int basicComparison = super.compareTo(other); + if (basicComparison != 0) { + return basicComparison; + } + WeightedAnswerSet otherWeighted = (WeightedAnswerSet) other; + return compareWeights(otherWeighted); + } + + @Override + public int hashCode() { + return Objects.hash(super.hashCode(), weightPerLevel); + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (!(o instanceof WeightedAnswerSet)) { + return false; + } + + WeightedAnswerSet that = (WeightedAnswerSet) o; + + if (!getPredicates().equals(that.getPredicates())) { + return false; + } + + if (!getPredicateInstances().equals(that.getPredicateInstances())) { + return false; + } + + return weightPerLevel.equals(that.weightPerLevel); + } + + public String getWeightsAsString() { + StringJoiner joiner = new StringJoiner(", ", "[", "]"); + for (Map.Entry weightPerLevel : weightPerLevel.entrySet()) { + joiner.add(weightPerLevel.getValue() + "@" + weightPerLevel.getKey()); + } + return joiner.toString(); + } + + /** + * Extract weights at levels from string of comma-separated pairs of the form weight@level. + * Multiple weights for the same level are summed-up. + * @param weightAtLevels + * @return a TreeMap containing + */ + public static TreeMap weightPerLevelFromString(String weightAtLevels) { + String[] weightsAtLevels = weightAtLevels.split(","); + TreeMap weightAtLevelsTreeMap = new TreeMap<>(); + for (String weightsAtLevel : weightsAtLevels) { + String[] wAtL = weightsAtLevel.trim().split("@"); + if (wAtL.length != 2) { + throw new IllegalArgumentException("Could not parse given comma-separated list of weight@level pairs. Given input was: " + weightAtLevels); + } + int weight = Integer.parseInt(wAtL[0]); + int level = Integer.parseInt(wAtL[1]); + if (weight == 0) { + continue; // Skip zero weights. + } + weightAtLevelsTreeMap.putIfAbsent(level, 0); + weightAtLevelsTreeMap.put(level, weight + weightAtLevelsTreeMap.get(level)); + } + return weightAtLevelsTreeMap; + } + + @Override + public String toString() { + return super.toString() + getWeightsAsString(); + } +} diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/ASPCore2ProgramImpl.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/ASPCore2ProgramImpl.java index 6369053ac..538bd88ac 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/ASPCore2ProgramImpl.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/ASPCore2ProgramImpl.java @@ -27,31 +27,25 @@ */ package at.ac.tuwien.kr.alpha.commons.programs; -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; - import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.rules.Rule; import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head; +import java.util.Collections; +import java.util.List; + /** * Alpha-internal representation of an ASP program, i.e., a set of ASP rules. *

- * Copyright (c) 2017-2019, the Alpha Team. + * Copyright (c) 2017-2023, the Alpha Team. */ class ASPCore2ProgramImpl extends AbstractProgram> implements ASPCore2Program{ - static final ASPCore2ProgramImpl EMPTY = new ASPCore2ProgramImpl(Collections.emptyList(), Collections.emptyList(), new InlineDirectivesImpl()); - - ASPCore2ProgramImpl(List> rules, List facts, InlineDirectives inlineDirectives) { - super(rules, facts, inlineDirectives); - } + static final ASPCore2ProgramImpl EMPTY = new ASPCore2ProgramImpl(Collections.emptyList(), Collections.emptyList(), new InlineDirectivesImpl(), false); - ASPCore2ProgramImpl() { - super(new ArrayList<>(), new ArrayList<>(), new InlineDirectivesImpl()); + ASPCore2ProgramImpl(List> rules, List facts, InlineDirectives inlineDirectives, boolean containsWeakConstraints) { + super(rules, facts, inlineDirectives, containsWeakConstraints); } - } diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/AbstractProgram.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/AbstractProgram.java index f78ee2e80..dfc05bb0c 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/AbstractProgram.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/AbstractProgram.java @@ -1,14 +1,14 @@ package at.ac.tuwien.kr.alpha.commons.programs; -import java.util.Collections; -import java.util.List; - import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.rules.Rule; import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head; import at.ac.tuwien.kr.alpha.commons.util.Util; +import java.util.Collections; +import java.util.List; + /** * The parent type for all kinds of programs. Defines a program's basic structure (facts + rules + inlineDirectives) * @@ -21,11 +21,13 @@ public abstract class AbstractProgram> { private final List rules; private final List facts; private final InlineDirectives inlineDirectives; + private final boolean containsWeakConstraints; - public AbstractProgram(List rules, List facts, InlineDirectives inlineDirectives) { + public AbstractProgram(List rules, List facts, InlineDirectives inlineDirectives, boolean containsWeakConstraints) { this.rules = rules; this.facts = facts; this.inlineDirectives = inlineDirectives; + this.containsWeakConstraints = containsWeakConstraints; } public List getRules() { @@ -50,4 +52,7 @@ public String toString() { return Util.join(result, rules, ls, ls); } + public boolean containsWeakConstraints() { + return containsWeakConstraints; + } } diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/NormalProgramImpl.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/NormalProgramImpl.java index 8bbfc4365..e1e418f17 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/NormalProgramImpl.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/NormalProgramImpl.java @@ -1,12 +1,12 @@ package at.ac.tuwien.kr.alpha.commons.programs; -import java.util.List; - import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives; import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.rules.NormalRule; +import java.util.List; + /** * A program that only contains NormalRules. * @@ -14,8 +14,8 @@ */ class NormalProgramImpl extends AbstractProgram implements NormalProgram { - NormalProgramImpl(List rules, List facts, InlineDirectives inlineDirectives) { - super(rules, facts, inlineDirectives); + NormalProgramImpl(List rules, List facts, InlineDirectives inlineDirectives, boolean containsWeakConstraints) { + super(rules, facts, inlineDirectives, containsWeakConstraints); } } diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/Programs.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/Programs.java index 2bafac832..a4c975094 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/Programs.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/Programs.java @@ -1,8 +1,5 @@ package at.ac.tuwien.kr.alpha.commons.programs; -import java.util.ArrayList; -import java.util.List; - import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; import at.ac.tuwien.kr.alpha.api.programs.InlineDirectives; import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; @@ -11,6 +8,10 @@ import at.ac.tuwien.kr.alpha.api.programs.rules.Rule; import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head; import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules; +import at.ac.tuwien.kr.alpha.commons.programs.rules.WeakConstraint; + +import java.util.ArrayList; +import java.util.List; public final class Programs { @@ -22,8 +23,8 @@ public static ASPCore2Program emptyProgram() { return ASPCore2ProgramImpl.EMPTY; } - public static ASPCore2Program newASPCore2Program(List> rules, List facts, InlineDirectives inlineDirectives) { - return new ASPCore2ProgramImpl(rules, facts, inlineDirectives); + public static ASPCore2Program newASPCore2Program(List> rules, List facts, InlineDirectives inlineDirectives, boolean containsWeakConstraints) { + return new ASPCore2ProgramImpl(rules, facts, inlineDirectives, containsWeakConstraints); } public static ASPCore2ProgramBuilder builder() { @@ -34,16 +35,18 @@ public static ASPCore2ProgramBuilder builder(ASPCore2Program program) { return new ASPCore2ProgramBuilder(program); } - public static NormalProgram newNormalProgram(List rules, List facts, InlineDirectives inlineDirectives) { - return new NormalProgramImpl(rules, facts, inlineDirectives); + public static NormalProgram newNormalProgram(List rules, List facts, InlineDirectives inlineDirectives, boolean containsWeakConstraints) { + return new NormalProgramImpl(rules, facts, inlineDirectives, containsWeakConstraints); } public static NormalProgram toNormalProgram(ASPCore2Program inputProgram) { List normalRules = new ArrayList<>(); + boolean containsWeakConstraints = false; for (Rule r : inputProgram.getRules()) { normalRules.add(Rules.toNormalRule(r)); + containsWeakConstraints |= r instanceof WeakConstraint; } - return new NormalProgramImpl(normalRules, inputProgram.getFacts(), inputProgram.getInlineDirectives()); + return new NormalProgramImpl(normalRules, inputProgram.getFacts(), inputProgram.getInlineDirectives(), containsWeakConstraints); } public static InlineDirectives newInlineDirectives() { @@ -58,11 +61,13 @@ public static class ASPCore2ProgramBuilder { private List> rules = new ArrayList<>(); private List facts = new ArrayList<>(); private InlineDirectives inlineDirectives = new InlineDirectivesImpl(); + private boolean containsWeakConstraints; public ASPCore2ProgramBuilder(ASPCore2Program prog) { this.addRules(prog.getRules()); this.addFacts(prog.getFacts()); this.addInlineDirectives(prog.getInlineDirectives()); + this.containsWeakConstraints = prog.containsWeakConstraints(); } public ASPCore2ProgramBuilder() { @@ -99,7 +104,7 @@ public ASPCore2ProgramBuilder accumulate(ASPCore2Program prog) { } public ASPCore2Program build() { - return Programs.newASPCore2Program(this.rules, this.facts, this.inlineDirectives); + return Programs.newASPCore2Program(this.rules, this.facts, this.inlineDirectives, containsWeakConstraints); } } diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/atoms/AbstractAtom.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/atoms/AbstractAtom.java index 4a54b90f4..e3aefa93a 100644 --- a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/atoms/AbstractAtom.java +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/atoms/AbstractAtom.java @@ -27,9 +27,6 @@ */ package at.ac.tuwien.kr.alpha.commons.programs.atoms; -import java.util.List; -import java.util.Set; - import at.ac.tuwien.kr.alpha.api.grounder.Substitution; import at.ac.tuwien.kr.alpha.api.programs.Predicate; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; @@ -38,6 +35,9 @@ import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm; import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms; +import java.util.List; +import java.util.Set; + /** * An Atom is the common superclass of all representations of ASP atoms used by Alpha. */ @@ -79,7 +79,7 @@ public Set getOccurringVariables() { /** * Returns whether this atom is ground, i.e., variable-free. * - * @return true iff the terms of this atom contain no {@link VariableTermImpl}. + * @return true iff the terms of this atom contain no {@link VariableTerm}. */ @Override public abstract boolean isGround(); diff --git a/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/rules/WeakConstraint.java b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/rules/WeakConstraint.java new file mode 100644 index 000000000..f3dbcf023 --- /dev/null +++ b/alpha-commons/src/main/java/at/ac/tuwien/kr/alpha/commons/programs/rules/WeakConstraint.java @@ -0,0 +1,44 @@ +package at.ac.tuwien.kr.alpha.commons.programs.rules; + +import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; +import at.ac.tuwien.kr.alpha.api.programs.terms.Term; +import at.ac.tuwien.kr.alpha.commons.util.Util; + +import java.util.List; + +/** + * Represents a weak constraint. + * + * Copyright (c) 2020, the Alpha Team. + */ +public class WeakConstraint extends BasicRule { + + private final Term weight; + private final Term level; + private final List termList; + + public WeakConstraint(List body, Term weight, Term level, List termList) { + super(null, body); + this.weight = weight; + this.level = level; + this.termList = termList; + } + + public Term getWeight() { + return weight; + } + + public Term getLevel() { + return level; + } + + public List getTermList() { + return termList; + } + + @Override + public String toString() { + String weightInformation = Util.join("[" + weight + "@" + level + (termList.isEmpty() ? "" : ", "), termList, "]"); + return Util.join(":~ ", getBody(), "." + weightInformation); + } +} diff --git a/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/WeightedAnswerSetTest.java b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/WeightedAnswerSetTest.java new file mode 100644 index 000000000..fbe7961ac --- /dev/null +++ b/alpha-commons/src/test/java/at/ac/tuwien/kr/alpha/commons/WeightedAnswerSetTest.java @@ -0,0 +1,75 @@ +package at.ac.tuwien.kr.alpha.commons; + +import at.ac.tuwien.kr.alpha.api.AnswerSet; +import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms; +import org.junit.jupiter.api.Test; + +import static at.ac.tuwien.kr.alpha.commons.WeightedAnswerSet.weightPerLevelFromString; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertNotEquals; + +/** + * Copyright (c) 2021, the Alpha Team. + */ +public class WeightedAnswerSetTest { + + @Test + public void compareWeightedAnswerSets() { + AnswerSet answerSet1 = new AnswerSetBuilder().predicate("a").instance().predicate("p").instance(Terms.newSymbolicConstant("b")).build(); + AnswerSet answerSet2 = new AnswerSetBuilder().predicate("a").instance().build(); + WeightedAnswerSet was1 = new WeightedAnswerSet(answerSet1, weightPerLevelFromString("1@1")); + WeightedAnswerSet was2 = new WeightedAnswerSet(answerSet2, weightPerLevelFromString("1@1, 2@3")); + WeightedAnswerSet was1Same = new WeightedAnswerSet(answerSet1, weightPerLevelFromString("1@1")); + + assertFalse(was1.getPredicates().isEmpty()); + assertFalse(was2.getPredicates().isEmpty()); + assertNotEquals(was1, was2); + assertEquals(was1Same, was1); + assertEquals(was1.getPredicateInstances(), was1Same.getPredicateInstances()); + } + + @Test + public void compareAnswerSetsSameAtoms() { + AnswerSet answerSet = new AnswerSetBuilder().predicate("q").instance(Terms.newConstant(0), Terms.newConstant(1)) + .predicate("b").instance().predicate("foo").instance(Terms.newSymbolicConstant("a")).build(); + WeightedAnswerSet was3 = new WeightedAnswerSet(answerSet, weightPerLevelFromString("1@1, 2@3")); + WeightedAnswerSet was3AtomsNotWeights = new WeightedAnswerSet(answerSet, weightPerLevelFromString("2@1, 2@3")); + + assertFalse(was3.getPredicates().isEmpty()); + assertNotEquals(was3, was3AtomsNotWeights); + assertEquals(was3.getPredicateInstances(), was3AtomsNotWeights.getPredicateInstances()); + } + + @Test + public void compareAnswerSetsSameWeights() { + String was4Weights = "1@1, 4@3"; + AnswerSet answerSetBC = new AnswerSetBuilder().predicate("b").instance().predicate("c").instance().build(); + AnswerSet answerSetBD = new AnswerSetBuilder().predicate("b").instance().predicate("d").instance().build(); + WeightedAnswerSet was4 = new WeightedAnswerSet(answerSetBC, weightPerLevelFromString(was4Weights)); + WeightedAnswerSet was5 = new WeightedAnswerSet(answerSetBD, weightPerLevelFromString(was4Weights)); + + assertFalse(was4.getPredicates().isEmpty()); + assertFalse(was5.getPredicates().isEmpty()); + assertEquals(0, was4.compareWeights(was5)); + assertNotEquals(was4, was5); + assertNotEquals(was5, was4); + } + + @Test + public void compareWeights() { + AnswerSet answerSet = new AnswerSetBuilder().predicate("a").instance().build(); + WeightedAnswerSet was6 = new WeightedAnswerSet(answerSet, weightPerLevelFromString("2@3")); + WeightedAnswerSet was7 = new WeightedAnswerSet(answerSet, weightPerLevelFromString("1@1, 1@3")); + WeightedAnswerSet was8 = new WeightedAnswerSet(answerSet, weightPerLevelFromString("1@-3, 1@1, 1@3")); + assertEquals(-1, was7.compareWeights(was6)); + assertEquals(1, was6.compareWeights(was7)); + + assertEquals(-1, was7.compareWeights(was8)); + assertEquals(1, was8.compareWeights(was7)); + + assertEquals(-1, was8.compareWeights(was6)); + assertEquals(1, was6.compareWeights(was8)); + } + +} \ No newline at end of file diff --git a/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 b/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 index 4f80be1a2..544e27500 100644 --- a/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 +++ b/alpha-core/src/main/antlr/at/ac/tuwien/kr/alpha/core/antlr/ASPCore2.g4 @@ -40,7 +40,7 @@ aggregate_element : basic_terms? (COLON naf_literals?)?; aggregate_function : AGGREGATE_COUNT | AGGREGATE_MAX | AGGREGATE_MIN | AGGREGATE_SUM; -weight_at_level : term (AT term)? (COMMA terms)?; +weight_at_level : weight=term (AT level=term)? (COMMA termlist=terms)?; naf_literals : naf_literal (COMMA naf_literals)?; diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java index d6cdecbb9..c21d0d556 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/Grounder.java @@ -27,10 +27,12 @@ */ package at.ac.tuwien.kr.alpha.core.grounder; +import java.util.List; import java.util.Map; import java.util.Set; import org.apache.commons.lang3.tuple.Pair; +import org.apache.commons.lang3.tuple.Triple; import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.core.common.Assignment; @@ -61,6 +63,20 @@ public interface Grounder { */ Pair, Map> getChoiceAtoms(); + /** + * States whether the input program given to the grounder contains weak constraints (which enables optimization). + * @return true if the input program to the grounder contains weak constraints. + */ + boolean inputProgramContainsWeakConstraints(); + + /** + * Returns the atomId of atoms representing weak constraints and the respective weights and levels. + * Must be preceded by a call to getNoGoods(). + * @return a list of triples (atomId, weight, level) where atomId is the atom that becomes true whenever the + * corresponding weak constraint is violated. + */ + List> getWeakConstraintInformation(); + /** * Updates the grounder with atoms assigned a positive truth value. * @param it an iterator over all newly assigned positive atoms. diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java index 2675337ce..c64a11a4b 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NaiveGrounder.java @@ -27,27 +27,6 @@ */ package at.ac.tuwien.kr.alpha.core.grounder; -import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; - -import java.util.ArrayList; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.LinkedHashMap; -import java.util.LinkedHashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.SortedSet; -import java.util.TreeSet; - -import org.apache.commons.lang3.tuple.ImmutablePair; -import org.apache.commons.lang3.tuple.Pair; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.config.GrounderHeuristicsConfiguration; import at.ac.tuwien.kr.alpha.api.grounder.Substitution; @@ -76,6 +55,27 @@ import at.ac.tuwien.kr.alpha.core.programs.atoms.ChoiceAtom; import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.core.programs.rules.CompiledRule; +import org.apache.commons.lang3.tuple.ImmutablePair; +import org.apache.commons.lang3.tuple.Pair; +import org.apache.commons.lang3.tuple.Triple; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; /** * A semi-naive grounder. @@ -90,6 +90,7 @@ public class NaiveGrounder extends BridgedGrounder implements ProgramAnalyzingGr private final NogoodRegistry registry = new NogoodRegistry(); final NoGoodGenerator noGoodGenerator; private final ChoiceRecorder choiceRecorder; + private final WeakConstraintRecorder weakConstraintRecorder; private final CompiledProgram program; private final AnalyzeUnjustified analyzeUnjustified; @@ -112,8 +113,8 @@ public NaiveGrounder(CompiledProgram program, AtomStore atomStore, boolean debug this(program, atomStore, new GrounderHeuristicsConfiguration(), debugInternalChecks, bridges); } - private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeuristicsConfiguration heuristicsConfiguration, boolean debugInternalChecks, - Bridge... bridges) { + private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeuristicsConfiguration heuristicsConfiguration, + boolean debugInternalChecks, Bridge... bridges) { this(program, atomStore, p -> true, heuristicsConfiguration, debugInternalChecks, bridges); } @@ -135,8 +136,8 @@ private NaiveGrounder(CompiledProgram program, AtomStore atomStore, GrounderHeur final Set uniqueGroundRulePerGroundHead = getRulesWithUniqueHead(); choiceRecorder = new ChoiceRecorder(atomStore); - noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, this.program, uniqueGroundRulePerGroundHead); - + weakConstraintRecorder = new WeakConstraintRecorder(); + noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, weakConstraintRecorder, factsFromProgram, this.program, uniqueGroundRulePerGroundHead); this.debugInternalChecks = debugInternalChecks; // Initialize RuleInstantiator and instantiation strategy. Note that the instantiation strategy also @@ -204,7 +205,7 @@ private Set getRulesWithUniqueHead() { } // Collect head and body variables. - HashSet occurringVariablesHead = new HashSet<>(headAtom.toLiteral().getBindingVariables()); + HashSet occurringVariablesHead = new HashSet<>(headAtom.getOccurringVariables()); HashSet occurringVariablesBody = new HashSet<>(); for (Literal lit : nonGroundRule.getPositiveBody()) { occurringVariablesBody.addAll(lit.getBindingVariables()); @@ -221,7 +222,7 @@ private Set getRulesWithUniqueHead() { /** * Registers a starting literal of a NonGroundRule at its corresponding working memory. - * + * * @param nonGroundRule the rule in which the literal occurs. */ private void registerLiteralAtWorkingMemory(Literal literal, CompiledRule nonGroundRule) { @@ -291,7 +292,7 @@ public AnswerSet assignmentToAnswerSet(Iterable trueAtoms) { /** * Prepares facts of the input program for joining and derives all NoGoods representing ground rules. May only be called once. - * + * * @return */ protected HashMap bootstrap() { @@ -429,8 +430,8 @@ BindingResult getGroundInstantiations(CompiledRule rule, RuleGroundingOrder grou for (int i = 0; i < bindingResult.size(); i++) { Integer numberOfUnassignedPositiveBodyAtoms = bindingResult.getNumbersOfUnassignedPositiveBodyAtoms().get(i); if (numberOfUnassignedPositiveBodyAtoms > 0) { - LOGGER.debug("Grounded rule in which {} positive atoms are still unassigned: {} (substitution: {})", numberOfUnassignedPositiveBodyAtoms, - rule, bindingResult.getGeneratedSubstitutions().get(i)); + LOGGER.debug("Grounded rule in which {} positive atoms are still unassigned: {} (substitution: {})", + numberOfUnassignedPositiveBodyAtoms, rule, bindingResult.getGeneratedSubstitutions().get(i)); } } } @@ -499,7 +500,7 @@ private BindingResult pushBackAndBindNextAtomInRule(RuleGroundingOrder grounding * Computes ground substitutions for the literal at position orderPosition of groundingOrder * Actual substitutions are computed by this grounder's {@link LiteralInstantiator}. * - * @param groundingOrder a {@link RuleGroundingOrderImpl} representing the body literals of a rule in the + * @param groundingOrder a {@link RuleGroundingOrderImpl} representing the body literals of a rule in the * sequence in which the should be bound during grounding. * @param orderPosition the current position within groundingOrder, indicates which literal should be bound * @param originalTolerance the original tolerance of the used grounding heuristic @@ -547,9 +548,8 @@ private BindingResult bindNextAtomInRule(RuleGroundingOrder groundingOrder, int * use, push the current literal to the end of the grounding order and proceed with the next one, otherwise return an empty BindingResult. */ if (originalTolerance > 0) { - LOGGER.trace( - "No substitutions yielded by literal instantiator for literal {}, but using permissive heuristic, therefore pushing the literal back.", - currentLiteral); + LOGGER.trace("No substitutions yielded by literal instantiator for literal {}," + + " but using permissive heuristic, therefore pushing the literal back.", currentLiteral); // This occurs when the grounder heuristic in use is a "permissive" one, // i.e. it is deemed acceptable to have ground rules where a number of body atoms are not yet assigned a truth value by the solver. return pushBackAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, partialSubstitution); @@ -570,11 +570,21 @@ public Pair, Map> getChoiceAtoms() { return choiceRecorder.getAndResetChoices(); } + @Override + public boolean inputProgramContainsWeakConstraints() { + return program.containsWeakConstraints(); + } + @Override public Map> getHeadsToBodies() { return choiceRecorder.getAndResetHeadsToBodies(); } + @Override + public List> getWeakConstraintInformation() { + return weakConstraintRecorder.getAndResetWeakConstraintAtomWeightLevels(); + } + @Override public void updateAssignment(IntIterator it) { while (it.hasNext()) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java index 1b06cdec3..b648fb6e6 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/NoGoodGenerator.java @@ -27,25 +27,13 @@ */ package at.ac.tuwien.kr.alpha.core.grounder; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.negateLiteral; -import static java.util.Collections.emptyList; -import static java.util.Collections.singletonList; - -import java.util.ArrayList; -import java.util.HashSet; -import java.util.LinkedHashSet; -import java.util.List; -import java.util.Map; -import java.util.Set; - import at.ac.tuwien.kr.alpha.api.grounder.Substitution; import at.ac.tuwien.kr.alpha.api.programs.Predicate; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; import at.ac.tuwien.kr.alpha.api.programs.literals.FixedInterpretationLiteral; import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; import at.ac.tuwien.kr.alpha.commons.substitutions.Instance; +import at.ac.tuwien.kr.alpha.core.atoms.WeakConstraintAtom; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.NoGood; import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram; @@ -53,6 +41,20 @@ import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.core.programs.rules.CompiledRule; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.negateLiteral; +import static java.util.Collections.emptyList; +import static java.util.Collections.singletonList; + /** * Class to generate ground NoGoods out of non-ground rules and grounding substitutions. * Copyright (c) 2017-2018, the Alpha Team. @@ -60,13 +62,15 @@ public class NoGoodGenerator { private final AtomStore atomStore; private final ChoiceRecorder choiceRecorder; + private final WeakConstraintRecorder weakConstraintRecorder; private final Map> factsFromProgram; private final CompiledProgram programAnalysis; private final Set uniqueGroundRulePerGroundHead; - NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, Map> factsFromProgram, CompiledProgram programAnalysis, Set uniqueGroundRulePerGroundHead) { + NoGoodGenerator(AtomStore atomStore, ChoiceRecorder recorder, WeakConstraintRecorder weakConstraintRecorder, Map> factsFromProgram, CompiledProgram programAnalysis, Set uniqueGroundRulePerGroundHead) { this.atomStore = atomStore; this.choiceRecorder = recorder; + this.weakConstraintRecorder = weakConstraintRecorder; this.factsFromProgram = factsFromProgram; this.programAnalysis = programAnalysis; this.uniqueGroundRulePerGroundHead = uniqueGroundRulePerGroundHead; @@ -95,9 +99,13 @@ List generateNoGoodsFromGroundSubstitution(final CompiledRule nonGroundR return singletonList(NoGood.fromConstraint(posLiterals, negLiterals)); } - final List result = new ArrayList<>(); - final Atom groundHeadAtom = nonGroundRule.getHeadAtom().substitute(substitution); + + if (groundHeadAtom instanceof WeakConstraintAtom) { + return generateWeakConstraintNogoods(posLiterals, negLiterals, groundHeadAtom); + } + + final List result = new ArrayList<>(); final int headId = atomStore.putIfAbsent(groundHeadAtom); // Prepare atom representing the rule body. @@ -140,6 +148,21 @@ List generateNoGoodsFromGroundSubstitution(final CompiledRule nonGroundR return result; } + private List generateWeakConstraintNogoods(List posLiterals, List negLiterals, Atom groundHeadAtom) { + int headId; + if (!atomStore.contains(groundHeadAtom)) { + headId = atomStore.putIfAbsent(groundHeadAtom); + // Record weak constraint association only the first time it is encountered. + WeakConstraintAtom weakConstraintAtom = (WeakConstraintAtom) groundHeadAtom; + weakConstraintRecorder.addWeakConstraint(headId, weakConstraintAtom.getWeight(), weakConstraintAtom.getLevel()); + } else { + headId = atomStore.get(groundHeadAtom); + } + // Treat weak constraints: generate NoGood for the if-direction (body satisfied causes head to be true). + NoGood wcRule = NoGood.fromBodyInternal(posLiterals, negLiterals, atomToLiteral(headId)); + return Collections.singletonList(wcRule); + } + List collectNegLiterals(final CompiledRule nonGroundRule, final Substitution substitution) { final List bodyLiteralsNegative = new ArrayList<>(); for (Literal lit : nonGroundRule.getNegativeBody()) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WeakConstraintRecorder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WeakConstraintRecorder.java new file mode 100644 index 000000000..42adc3ff3 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/grounder/WeakConstraintRecorder.java @@ -0,0 +1,31 @@ +package at.ac.tuwien.kr.alpha.core.grounder; + +import org.apache.commons.lang3.tuple.ImmutableTriple; +import org.apache.commons.lang3.tuple.Triple; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + +/** + * Temporarily stores associations of weak constraint atoms, and their weights and levels. + * + * Copyright (c) 2020, the Alpha Team. + */ +class WeakConstraintRecorder { + + private ArrayList> weakConstraintAtomWeightLevels = new ArrayList<>(); + + void addWeakConstraint(int headId, Integer weight, Integer level) { + weakConstraintAtomWeightLevels.add(new ImmutableTriple<>(headId, weight, level)); + } + + List> getAndResetWeakConstraintAtomWeightLevels() { + if (weakConstraintAtomWeightLevels.isEmpty()) { + return Collections.emptyList(); + } + List> currentWeakConstraintAtomWeightLevels = weakConstraintAtomWeightLevels; + this.weakConstraintAtomWeightLevels = new ArrayList<>(); + return currentWeakConstraintAtomWeightLevels; + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java index 5d77e587d..c7d829f14 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/parser/ParseTreeVisitor.java @@ -27,19 +27,6 @@ */ package at.ac.tuwien.kr.alpha.core.parser; -import java.util.ArrayList; -import java.util.Collections; -import java.util.LinkedList; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.SortedSet; -import java.util.TreeMap; -import java.util.TreeSet; - -import org.antlr.v4.runtime.RuleContext; -import org.antlr.v4.runtime.tree.TerminalNode; - import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.ComparisonOperator; import at.ac.tuwien.kr.alpha.api.common.fixedinterpretations.PredicateInterpretation; @@ -71,10 +58,25 @@ import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.programs.literals.Literals; import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules; +import at.ac.tuwien.kr.alpha.commons.programs.rules.WeakConstraint; import at.ac.tuwien.kr.alpha.commons.programs.rules.heads.Heads; import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms; import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2BaseVisitor; import at.ac.tuwien.kr.alpha.core.antlr.ASPCore2Parser; +import org.antlr.v4.runtime.RuleContext; +import org.antlr.v4.runtime.tree.TerminalNode; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeMap; +import java.util.TreeSet; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; /** * Copyright (c) 2016-2018, the Alpha Team. @@ -207,7 +209,19 @@ public Object visitStatement_rule(ASPCore2Parser.Statement_ruleContext ctx) { @Override public Object visitStatement_weightConstraint(ASPCore2Parser.Statement_weightConstraintContext ctx) { // WCONS body? DOT SQUARE_OPEN weight_at_level SQUARE_CLOSE - throw notSupported(ctx); + List bodyLiterals = ctx.body() != null ? visitBody(ctx.body()) : Collections.emptyList(); + Term weight = (Term)visit(ctx.weight_at_level().weight); + Term level = ctx.weight_at_level().level != null ? (Term)visit(ctx.weight_at_level().level) : null; + List termList = ctx.weight_at_level().termlist != null ? visitTerms(ctx.weight_at_level().termlist) : null; + programBuilder.addRule(new WeakConstraint(bodyLiterals, weight, level, termList)); + return null; + } + + @Override + public Object visitWeight_at_level(ASPCore2Parser.Weight_at_levelContext ctx) { + // weight_at_level : term (AT term)? (COMMA terms)?; + // Construction fully done at visitStatement_weightConstraint, should never descend to this. + throw oops("ParserTreeVisitor called method visitWeight_at_level."); } @Override @@ -497,7 +511,7 @@ public ConstantTerm visitTerm_number(ASPCore2Parser.Term_numberContext return Terms.newConstant(visitNumeral(ctx.numeral())); } - public Integer visitNumeral(ASPCore2Parser.NumeralContext ctx) { + public Integer visitNumeral(ASPCore2Parser.NumeralContext ctx) { // numeral : MINUS? NUMBER; int absValue = Integer.valueOf(ctx.NUMBER().getText()); return ctx.MINUS() != null ? -1 * absValue : absValue; @@ -573,7 +587,7 @@ public IntervalTerm visitTerm_interval(ASPCore2Parser.Term_intervalContext ctx) return Terms.newIntervalTerm(lower, upper); } - @Override + @Override public Term visitInterval_bound(ASPCore2Parser.Interval_boundContext ctx) { // interval_bound : numeral | VARIABLE; if (ctx.numeral() != null) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/AnalyzedProgram.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/AnalyzedProgram.java index e3dd5336e..e6f312549 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/AnalyzedProgram.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/AnalyzedProgram.java @@ -5,7 +5,7 @@ import at.ac.tuwien.kr.alpha.api.programs.analysis.ComponentGraph; import at.ac.tuwien.kr.alpha.api.programs.analysis.DependencyGraph; import at.ac.tuwien.kr.alpha.core.depgraph.DependencyGraphImpl; -import org.apache.commons.lang3.tuple.ImmutablePair; +import org.apache.commons.lang3.tuple.ImmutableTriple; import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; @@ -24,15 +24,15 @@ public class AnalyzedProgram extends InternalProgram { private final DependencyGraph dependencyGraph; private final ComponentGraph componentGraph; - public AnalyzedProgram(List rules, List facts) { - super(rules, facts); + public AnalyzedProgram(List rules, List facts, Boolean containsWeakConstraints) { + super(rules, facts, containsWeakConstraints); dependencyGraph = DependencyGraphImpl.buildDependencyGraph(getRulesById()); componentGraph = buildComponentGraph(dependencyGraph); } public static AnalyzedProgram analyzeNormalProgram(NormalProgram prog) { - ImmutablePair, List> rulesAndFacts = InternalProgram.internalizeRulesAndFacts(prog); - return new AnalyzedProgram(rulesAndFacts.left, rulesAndFacts.right); + ImmutableTriple, List, Boolean> rulesAndFacts = InternalProgram.internalizeRulesAndFacts(prog); + return new AnalyzedProgram(rulesAndFacts.left, rulesAndFacts.middle, rulesAndFacts.right); } private ComponentGraph buildComponentGraph(DependencyGraph depGraph) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/InternalProgram.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/InternalProgram.java index 43e69b984..fb2df71d1 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/InternalProgram.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/InternalProgram.java @@ -7,7 +7,7 @@ import java.util.List; import java.util.Map; -import org.apache.commons.lang3.tuple.ImmutablePair; +import org.apache.commons.lang3.tuple.ImmutableTriple; import at.ac.tuwien.kr.alpha.api.programs.NormalProgram; import at.ac.tuwien.kr.alpha.api.programs.Predicate; @@ -19,6 +19,7 @@ import at.ac.tuwien.kr.alpha.commons.programs.Programs; import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules; import at.ac.tuwien.kr.alpha.commons.substitutions.Instance; +import at.ac.tuwien.kr.alpha.core.atoms.WeakConstraintAtom; import at.ac.tuwien.kr.alpha.core.grounder.FactIntervalEvaluator; import at.ac.tuwien.kr.alpha.core.programs.rules.CompiledRule; import at.ac.tuwien.kr.alpha.core.programs.rules.InternalRule; @@ -28,7 +29,7 @@ * aggregates must be rewritten, all intervals must be preprocessed (into interval atoms), and equality predicates must * be rewritten. *

- * Copyright (c) 2017-2021, the Alpha Team. + * Copyright (c) 2017-2023, the Alpha Team. */ public class InternalProgram extends AbstractProgram implements CompiledProgram { @@ -36,15 +37,16 @@ public class InternalProgram extends AbstractProgram implements Co private final Map> factsByPredicate = new LinkedHashMap<>(); private final Map rulesById = new LinkedHashMap<>(); - public InternalProgram(List rules, List facts) { - super(rules, facts, null); + public InternalProgram(List rules, List facts, boolean containsWeakConstraints) { + super(rules, facts, null, containsWeakConstraints); recordFacts(facts); recordRules(rules); } - static ImmutablePair, List> internalizeRulesAndFacts(NormalProgram normalProgram) { + static ImmutableTriple, List, Boolean> internalizeRulesAndFacts(NormalProgram normalProgram) { List internalRules = new ArrayList<>(); List facts = new ArrayList<>(normalProgram.getFacts()); + boolean containsWeakConstraints = false; for (Rule r : normalProgram.getRules()) { if (r.getBody().isEmpty()) { if (!r.getHead().isGround()) { @@ -53,14 +55,17 @@ static ImmutablePair, List> internalizeRulesAndFacts(No facts.add(r.getHead().getAtom()); } else { internalRules.add(InternalRule.fromNormalRule(r)); + if (!r.isConstraint() && r.getHead().getAtom() instanceof WeakConstraintAtom) { + containsWeakConstraints = true; + } } } - return new ImmutablePair<>(internalRules, facts); + return new ImmutableTriple<>(internalRules, facts, containsWeakConstraints); } public static InternalProgram fromNormalProgram(NormalProgram normalProgram) { - ImmutablePair, List> rulesAndFacts = InternalProgram.internalizeRulesAndFacts(normalProgram); - return new InternalProgram(rulesAndFacts.left, rulesAndFacts.right); + ImmutableTriple, List, Boolean> rulesAndFacts = InternalProgram.internalizeRulesAndFacts(normalProgram); + return new InternalProgram(rulesAndFacts.left, rulesAndFacts.middle, rulesAndFacts.right); } private void recordFacts(List facts) { @@ -106,7 +111,6 @@ public NormalProgram toNormalProgram() { for (CompiledRule rule : getRules()) { normalRules.add(Rules.newNormalRule(rule.getHead(), new ArrayList<>(rule.getBody()))); } - return Programs.newNormalProgram(normalRules, getFacts(), getInlineDirectives()); + return Programs.newNormalProgram(normalRules, getFacts(), getInlineDirectives(), containsWeakConstraints()); } - } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/atoms/WeakConstraintAtom.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/atoms/WeakConstraintAtom.java new file mode 100644 index 000000000..1d4e403de --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/atoms/WeakConstraintAtom.java @@ -0,0 +1,167 @@ +package at.ac.tuwien.kr.alpha.core.atoms; + +import at.ac.tuwien.kr.alpha.api.grounder.Substitution; +import at.ac.tuwien.kr.alpha.api.programs.Predicate; +import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; +import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; +import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; +import at.ac.tuwien.kr.alpha.api.programs.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.api.programs.terms.FunctionTerm; +import at.ac.tuwien.kr.alpha.api.programs.terms.Term; +import at.ac.tuwien.kr.alpha.api.programs.terms.VariableTerm; +import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.programs.atoms.AbstractAtom; +import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Objects; +import java.util.Set; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; + +/** + * Represents the head of a weak constraint (i.e., a special internal atom indicating that a rule really is a weak + * constraint). + * + * Copyright (c) 2020-2021, the Alpha Team. + */ +public class WeakConstraintAtom extends AbstractAtom implements BasicAtom { + private static final Predicate PREDICATE = Predicates.getPredicate("_weakconstraint_", 3, true, true); + private static final String TERMLISTSYMBOL = "_tuple"; + + private final Term weight; + private final Term level; + private final FunctionTerm termList; + + private WeakConstraintAtom(Term weight, Term level, FunctionTerm termList) { + if (!isIntegerOrVariable(weight)) { + throw new IllegalArgumentException("WeakConstraint with non-integer weight encountered: " + weight); + } + if (isNegativeInteger(weight)) { + throw new IllegalArgumentException("WeakConstraint with negative weight encountered: " + weight + "@" + level + "\n" + + "Negative weights in weak constraints are not supported. Please rewrite your input program (turn negative weight if condition is met into positive weight if inverse condition is met)."); + } + if (!isIntegerOrVariable(level)) { + throw new IllegalArgumentException("WeakConstraint with non-integer level encountered: " + level); + } + this.weight = weight; + this.level = level; + this.termList = termList; + } + + public static WeakConstraintAtom getInstance(Term weight, Term level, List termList) { + Term actualLevel = level != null ? level : Terms.newConstant(0); + List actualTermlist = termList != null ? termList : Collections.emptyList(); + return new WeakConstraintAtom(weight, actualLevel, Terms.newFunctionTerm(TERMLISTSYMBOL, actualTermlist)); + } + + public Integer getWeight() { + return (Integer) ((ConstantTerm)weight).getObject(); + } + + public Integer getLevel() { + return (Integer) ((ConstantTerm)level).getObject(); + } + + private static boolean isIntegerOrVariable(Term term) { + if (term instanceof VariableTerm) { + return true; + } + if (term instanceof ConstantTerm) { + Comparable constant = ((ConstantTerm) term).getObject(); + return constant instanceof Integer; + } + return false; + } + + private static boolean isNegativeInteger(Term term) { + if (term instanceof ConstantTerm && ((ConstantTerm) term).getObject() instanceof Integer) { + return ((Integer)((ConstantTerm) term).getObject()) < 0; + } + return false; + } + + @Override + public Predicate getPredicate() { + return PREDICATE; + } + + @Override + public List getTerms() { + List ret = new ArrayList<>(3); + ret.add(weight); + ret.add(level); + ret.add(termList); + return ret; + } + + @Override + public Atom withTerms(List terms) { + if (terms.size() != 3) { + throw oops("Trying to create WeakConstraintAtom with other than 3 terms."); + } + if (!(terms.get(2) instanceof FunctionTerm) || !((FunctionTerm) terms.get(2)).getSymbol().equals(TERMLISTSYMBOL)) { + throw oops("Trying to create WeakConstraintAtom with 3rd term not being the correct function term."); + } + return new WeakConstraintAtom(terms.get(0), terms.get(1), (FunctionTerm) terms.get(2)); + } + + @Override + public boolean isGround() { + return weight.isGround() && level.isGround() && termList.isGround(); + } + + @Override + public WeakConstraintAtom substitute(Substitution substitution) { + if (isGround()) { + return this; + } + return new WeakConstraintAtom(weight.substitute(substitution), level.substitute(substitution), (FunctionTerm) termList.substitute(substitution)); + } + + @Override + public Set getOccurringVariables() { + Set occurringVariables = new HashSet<>(); + occurringVariables.addAll(weight.getOccurringVariables()); + occurringVariables.addAll(level.getOccurringVariables()); + occurringVariables.addAll(termList.getOccurringVariables()); + return occurringVariables; + } + + @Override + public String toString() { + return PREDICATE.getName() + "(" + weight + "@" + level + ", " + termList + ")"; + } + + @Override + public Literal toLiteral(boolean positive) { + throw new UnsupportedOperationException("WeakConstraintAtom cannot be literalized."); + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + WeakConstraintAtom that = (WeakConstraintAtom) o; + return weight.equals(that.weight) && + level.equals(that.level) && + termList.equals(that.termList); + } + + @Override + public int hashCode() { + return Objects.hash(weight, level, termList); + } + + @Override + public Atom normalizeVariables(String prefix, int counterStartingValue) { + throw new UnsupportedOperationException("WeakConstraintAtom cannot normalize its variables."); + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java index b556c642a..48cb26091 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/ArithmeticTermsRewriting.java @@ -52,7 +52,7 @@ public NormalProgram apply(NormalProgram inputProgram) { return inputProgram; } // Create new program with rewritten rules. - return Programs.newNormalProgram(rewrittenRules, inputProgram.getFacts(), inputProgram.getInlineDirectives()); + return Programs.newNormalProgram(rewrittenRules, inputProgram.getFacts(), inputProgram.getInlineDirectives(), inputProgram.containsWeakConstraints()); } /** diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java index 90d532aff..d7e3d12b9 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/IntervalTermToIntervalAtom.java @@ -79,7 +79,7 @@ private static NormalRule rewriteIntervalSpecifications(NormalRule rule) { // Note that this cast is safe: NormalHead can only have a BasicAtom, so literalizing and getting back the Atom destroys type information, // but should never yield anything other than a BasicAtom NormalHead rewrittenHead = rule.isConstraint() ? null - : Heads.newNormalHead((BasicAtom) rewriteLiteral(rule.getHead().getAtom().toLiteral(), intervalReplacements).getAtom()); + : Heads.newNormalHead((BasicAtom) rewriteAtom(rule.getHead().getAtom(), intervalReplacements)); // If intervalReplacements is empty, no IntervalTerms have been found, keep rule as is. if (intervalReplacements.isEmpty()) { @@ -95,7 +95,7 @@ private static NormalRule rewriteIntervalSpecifications(NormalRule rule) { /** * Replaces every IntervalTerm by a new variable and returns a mapping of the replaced VariableTerm -> IntervalTerm. - * + * * @return the rewritten literal or null if the literal should be dropped from the final rule. */ private static Literal rewriteLiteral(Literal lit, Map intervalReplacement) { @@ -115,6 +115,14 @@ private static Literal rewriteLiteral(Literal lit, Map intervalReplacement) { List termList = new ArrayList<>(atom.getTerms()); boolean didChange = false; for (int i = 0; i < termList.size(); i++) { @@ -133,10 +141,9 @@ private static Literal rewriteLiteral(Literal lit, Map intervalReplacement) { @@ -182,6 +189,6 @@ public NormalProgram apply(NormalProgram inputProgram) { if (!didChange) { return inputProgram; } - return Programs.newNormalProgram(rewrittenRules, inputProgram.getFacts(), inputProgram.getInlineDirectives()); + return Programs.newNormalProgram(rewrittenRules, inputProgram.getFacts(), inputProgram.getInlineDirectives(), inputProgram.containsWeakConstraints()); } } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/NormalizeProgramTransformation.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/NormalizeProgramTransformation.java index f8d3303f0..a9670a766 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/NormalizeProgramTransformation.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/NormalizeProgramTransformation.java @@ -29,6 +29,8 @@ public NormalProgram apply(ASPCore2Program inputProgram) { tmpPrg = new ChoiceHeadToNormal().apply(tmpPrg); // Transform aggregates. tmpPrg = new AggregateRewriting(aggregateRewritingCfg.isUseSortingGridEncoding(), aggregateRewritingCfg.isSupportNegativeValuesInSums()).apply(tmpPrg); + // Transform weak constraints. + tmpPrg = new WeakConstraintNormalization().apply(tmpPrg); // Transform enumeration atoms. tmpPrg = new EnumerationRewriting().apply(tmpPrg); EnumerationAtom.resetEnumerations(); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java index 34fed23dc..cd575a7ed 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/StratifiedEvaluation.java @@ -97,7 +97,7 @@ public InternalProgram apply(AnalyzedProgram inputProgram) { .forEach((entry) -> outputRules.add(entry.getValue())); // NOTE: if InternalProgram requires solved rules, they should be added here. - return new InternalProgram(outputRules, additionalFacts); + return new InternalProgram(outputRules, additionalFacts, inputProgram.containsWeakConstraints()); } private void evaluateComponent(ComponentGraph.SCComponent comp) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/VariableEqualityRemoval.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/VariableEqualityRemoval.java index 3c84b54a0..bfddfd28c 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/VariableEqualityRemoval.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/VariableEqualityRemoval.java @@ -65,7 +65,7 @@ public ASPCore2Program apply(ASPCore2Program inputProgram) { for (Rule rule : inputProgram.getRules()) { rewrittenRules.add(findAndReplaceVariableEquality(rule)); } - return Programs.newASPCore2Program(rewrittenRules, inputProgram.getFacts(), inputProgram.getInlineDirectives()); + return Programs.newASPCore2Program(rewrittenRules, inputProgram.getFacts(), inputProgram.getInlineDirectives(), inputProgram.containsWeakConstraints()); } private Rule findAndReplaceVariableEquality(Rule rule) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/WeakConstraintNormalization.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/WeakConstraintNormalization.java new file mode 100644 index 000000000..7f38f375d --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/WeakConstraintNormalization.java @@ -0,0 +1,40 @@ +package at.ac.tuwien.kr.alpha.core.programs.transformation; + + +import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; +import at.ac.tuwien.kr.alpha.api.programs.rules.Rule; +import at.ac.tuwien.kr.alpha.api.programs.rules.heads.Head; +import at.ac.tuwien.kr.alpha.commons.programs.Programs; +import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules; +import at.ac.tuwien.kr.alpha.commons.programs.rules.WeakConstraint; +import at.ac.tuwien.kr.alpha.commons.programs.rules.heads.Heads; +import at.ac.tuwien.kr.alpha.core.atoms.WeakConstraintAtom; + +import java.util.ArrayList; + +/** + * Rewrites weak constraints into normal rules with special head atom. + * + * Copyright (c) 2020, the Alpha Team. + */ +public class WeakConstraintNormalization extends ProgramTransformation { + @Override + public ASPCore2Program apply(ASPCore2Program inputProgram) { + Programs.ASPCore2ProgramBuilder builder = Programs.builder(); + builder.addFacts(inputProgram.getFacts()); + builder.addInlineDirectives(inputProgram.getInlineDirectives()); + + for (Rule rule : inputProgram.getRules()) { + if (!(rule instanceof WeakConstraint)) { + builder.addRule(rule); + continue; + } + // Create rule with special head atom. + WeakConstraint weakConstraint = (WeakConstraint)rule; + Head weakConstraintHead = Heads.newNormalHead(WeakConstraintAtom.getInstance(weakConstraint.getWeight(), weakConstraint.getLevel(), weakConstraint.getTermList())); + Rule rewrittenWeakConstraint = Rules.newRule(weakConstraintHead, new ArrayList<>(rule.getBody())); + builder.addRule(rewrittenWeakConstraint); + } + return builder.build(); + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalization.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalization.java index 12e3273b6..dda7f5a0a 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalization.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/AggregateOperatorNormalization.java @@ -1,9 +1,5 @@ package at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates; -import java.util.ArrayList; -import java.util.Collections; -import java.util.List; - import at.ac.tuwien.kr.alpha.api.ComparisonOperator; import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom; import at.ac.tuwien.kr.alpha.api.programs.atoms.AggregateAtom.AggregateFunctionSymbol; @@ -19,8 +15,13 @@ import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.programs.literals.Literals; import at.ac.tuwien.kr.alpha.commons.programs.rules.Rules; +import at.ac.tuwien.kr.alpha.commons.programs.rules.WeakConstraint; import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms; +import java.util.ArrayList; +import java.util.Collections; +import java.util.List; + /** * Transforms an {@link AspCore2ProgramImpl} such that, for all aggregate (body-)literals, only the comparison operators "=" * and "<=" are used. @@ -41,7 +42,7 @@ * Note that input programs must only contain aggregate literals of form TERM OP #aggr{...} or #aggr{...} OP TERM, * i.e. with only * a left or right term and operator (but not both). When preprocessing programs, apply this transformation AFTER - * {@link at.ac.tuwien.kr.alpha.grounder.transformation.aggregates.AggregateLiteralSplitting}. + * {@link at.ac.tuwien.kr.alpha.core.programs.transformation.aggregates.AggregateLiteralSplitting}. * * Copyright (c) 2020-2021, the Alpha Team. */ @@ -56,6 +57,10 @@ public static Rule normalize(Rule rule) { for (Literal lit : rule.getBody()) { rewrittenBody.addAll(rewriteLiteral(lit)); } + if (rule instanceof WeakConstraint) { + WeakConstraint wcRule = (WeakConstraint) rule; + return new WeakConstraint(rewrittenBody, wcRule.getWeight(), wcRule.getLevel(), wcRule.getTermList()); + } return Rules.newRule(rule.getHead(), rewrittenBody); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/AbstractAggregateEncoder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/AbstractAggregateEncoder.java index 4b6c431b1..dd9744d3a 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/AbstractAggregateEncoder.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/AbstractAggregateEncoder.java @@ -82,7 +82,7 @@ public ASPCore2Program encodeAggregateLiteral(AggregateInfo aggregateToEncode) { Rule elementRule = encodeAggregateElement(aggregateToEncode, elementToEncode); elementEncodingRules.add(PredicateInternalizer.makePrefixedPredicatesInternal(elementRule, aggregateId)); } - return Programs.newASPCore2Program(ListUtils.union(literalEncoding.getRules(), elementEncodingRules), literalEncoding.getFacts(), Programs.newInlineDirectives()); + return Programs.newASPCore2Program(ListUtils.union(literalEncoding.getRules(), elementEncodingRules), literalEncoding.getFacts(), Programs.newInlineDirectives(), literalEncoding.containsWeakConstraints()); } /** diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/StringtemplateBasedAggregateEncoder.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/StringtemplateBasedAggregateEncoder.java index 8869c66fe..b47703691 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/StringtemplateBasedAggregateEncoder.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/programs/transformation/aggregates/encoders/StringtemplateBasedAggregateEncoder.java @@ -85,7 +85,7 @@ protected ASPCore2Program encodeAggregateResult(AggregateInfo aggregateToEncode) // Add the programatically created bound rule and return return Programs.newASPCore2Program(ListUtils.union(coreEncoding.getRules(), Collections.singletonList(boundRule)), coreEncoding.getFacts(), - Programs.newInlineDirectives()); + Programs.newInlineDirectives(), coreEncoding.containsWeakConstraints()); } private String getBoundPredicateName(String aggregateId) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCallbackManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCallbackManager.java new file mode 100644 index 000000000..8b636c1a0 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/AtomCallbackManager.java @@ -0,0 +1,59 @@ +package at.ac.tuwien.kr.alpha.core.solver; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.Arrays; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.arrayGrowthSize; +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; + +/** + * Manages the execution of {@link AtomCallback}s, i.e., callbacks when atoms change their truth value. + * + * Copyright (c) 2020, the Alpha Team. + */ +public class AtomCallbackManager { + + private static final Logger LOGGER = LoggerFactory.getLogger(AtomCallbackManager.class); + + private AtomCallback[] atomCallbacks = new AtomCallback[0]; + + public void recordCallback(int atom, AtomCallback atomCallback) { + if (atomCallbacks[atom] != null && !atomCallbacks[atom].equals(atomCallback)) { + throw oops("Recording different callbacks for one atom. Atom: " + atom); + } + atomCallbacks[atom] = atomCallback; + } + + void callbackOnChanged(int atom) { + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Callback received on callback atom: {}", atom); + } + AtomCallback atomCallback = atomCallbacks[atom]; + if (atomCallback != null) { + atomCallback.processCallback(); + } + } + + void growForMaxAtomId(int maxAtomId) { + // Grow arrays only if needed. + if (atomCallbacks.length > maxAtomId) { + return; + } + // Grow to default size, except if bigger array is required due to maxAtomId. + int newCapacity = arrayGrowthSize(atomCallbacks.length); + if (newCapacity < maxAtomId + 1) { + newCapacity = maxAtomId + 1; + } + atomCallbacks = Arrays.copyOf(atomCallbacks, newCapacity); + } + + /** + * Interface for callbacks to be called when atoms change their truth value. + */ + public interface AtomCallback { + + void processCallback(); + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java index 8ab9088d3..7e74ba37e 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceInfluenceManager.java @@ -96,6 +96,9 @@ private void addInformation(Map.Entry atomToEnabler, Map maxAtomId) { @@ -181,7 +174,7 @@ void setActivityListener(ActivityListener listener) { this.activityListener = listener; } - private class ChoicePoint { + private class ChoicePoint implements AtomCallbackManager.AtomCallback { final Integer atom; final int enabler; final int disabler; @@ -205,6 +198,11 @@ private boolean isNotChosen() { return atomTruth == null || atomTruth == MBT; } + @Override + public void processCallback() { + recomputeActive(); + } + void recomputeActive() { LOGGER.trace("Recomputing activity of atom {}.", atom); final boolean wasActive = isActive; @@ -232,7 +230,7 @@ public String toString() { } } - public static interface ActivityListener { + public interface ActivityListener { void callbackOnChanged(int atom, boolean active); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java index 343fe2eab..b415a6896 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/ChoiceManager.java @@ -79,7 +79,6 @@ public ChoiceManager(WritableAssignment assignment, NoGoodStore store) { this.assignment = assignment; this.choicePointInfluenceManager = new ChoiceInfluenceManager(assignment); this.choiceStack = new Stack<>(); - assignment.setCallback(this); this.bnpEstimation = store instanceof BinaryNoGoodPropagationEstimation ? (BinaryNoGoodPropagationEstimation)store : null; @@ -101,7 +100,7 @@ NoGood computeEnumeration() { @Override public void setChecksEnabled(boolean checksEnabled) { this.checksEnabled = checksEnabled; - this.choicePointInfluenceManager.setChecksEnabled(checksEnabled); + choicePointInfluenceManager.setChecksEnabled(checksEnabled); if (checksEnabled) { debugWatcher = new DebugWatcher(); @@ -114,10 +113,6 @@ public boolean isChecksEnabled() { return checksEnabled; } - public void callbackOnChanged(int atom) { - choicePointInfluenceManager.callbackOnChanged(atom); - } - public int getBackjumps() { return backjumps; } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java index ab5642ad8..4aa68271c 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/DefaultSolver.java @@ -27,28 +27,6 @@ */ package at.ac.tuwien.kr.alpha.core.solver; -import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToNegatedLiteral; -import static at.ac.tuwien.kr.alpha.core.solver.NoGoodStore.LBD_NO_VALUE; -import static at.ac.tuwien.kr.alpha.core.solver.heuristics.BranchingHeuristic.DEFAULT_CHOICE_LITERAL; -import static at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult.UNSAT; - -import java.util.ArrayList; -import java.util.Iterator; -import java.util.LinkedHashMap; -import java.util.LinkedHashSet; -import java.util.LinkedList; -import java.util.Map; -import java.util.Map.Entry; -import java.util.Random; -import java.util.Set; -import java.util.function.Consumer; - -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.StatisticsReportingSolver; import at.ac.tuwien.kr.alpha.api.config.SystemConfig; @@ -58,6 +36,7 @@ import at.ac.tuwien.kr.alpha.api.programs.atoms.ComparisonAtom; import at.ac.tuwien.kr.alpha.api.programs.literals.Literal; import at.ac.tuwien.kr.alpha.api.programs.terms.ConstantTerm; +import at.ac.tuwien.kr.alpha.commons.WeightedAnswerSet; import at.ac.tuwien.kr.alpha.core.common.AtomStore; import at.ac.tuwien.kr.alpha.core.common.NoGood; import at.ac.tuwien.kr.alpha.core.grounder.Grounder; @@ -70,6 +49,29 @@ import at.ac.tuwien.kr.alpha.core.solver.heuristics.HeuristicsConfiguration; import at.ac.tuwien.kr.alpha.core.solver.heuristics.NaiveHeuristic; import at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner; +import at.ac.tuwien.kr.alpha.core.solver.optimization.WeakConstraintsManager; +import at.ac.tuwien.kr.alpha.core.solver.optimization.WeakConstraintsManagerForUnboundedEnumeration; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.LinkedList; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Random; +import java.util.Set; +import java.util.function.Consumer; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToNegatedLiteral; +import static at.ac.tuwien.kr.alpha.core.solver.NoGoodStore.LBD_NO_VALUE; +import static at.ac.tuwien.kr.alpha.core.solver.heuristics.BranchingHeuristic.DEFAULT_CHOICE_LITERAL; +import static at.ac.tuwien.kr.alpha.core.solver.learning.GroundConflictNoGoodLearner.ConflictAnalysisResult.UNSAT; /** * The new default solver employed in Alpha. @@ -81,16 +83,17 @@ public class DefaultSolver extends AbstractSolver implements StatisticsReporting private final NoGoodStore store; private final ChoiceManager choiceManager; - private final WritableAssignment assignment; + protected final WritableAssignment assignment; private final GroundConflictNoGoodLearner learner; private final BranchingHeuristic branchingHeuristic; + protected WeakConstraintsManager weakConstraintsManager; private int mbtAtFixpoint; private int conflictsAfterClosing; private final boolean disableJustifications; private boolean disableJustificationAfterClosing = true; // Keep disabled for now, case not fully worked out yet. private final boolean disableNoGoodDeletion; - private static class SearchState { + protected static class SearchState { boolean hasBeenInitialized; boolean isSearchSpaceCompletelyExplored; /** @@ -98,13 +101,12 @@ private static class SearchState { */ boolean afterAllAtomsAssigned; } - private final SearchState searchState = new SearchState(); + protected final SearchState searchState = new SearchState(); - private final PerformanceLog performanceLog; + protected final PerformanceLog performanceLog; public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, WritableAssignment assignment, Random random, SystemConfig config, HeuristicsConfiguration heuristicsConfiguration) { super(atomStore, grounder); - this.assignment = assignment; this.store = store; this.choiceManager = new ChoiceManager(assignment, store); @@ -114,6 +116,8 @@ public DefaultSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, this.disableJustifications = config.isDisableJustificationSearch(); this.disableNoGoodDeletion = config.isDisableNoGoodDeletion(); this.performanceLog = new PerformanceLog(choiceManager, (TrailAssignment) assignment, 1000); + this.weakConstraintsManager = new WeakConstraintsManagerForUnboundedEnumeration(assignment); + this.weakConstraintsManager.setChecksEnabled(config.isDebugInternalChecks()); } private BranchingHeuristic chainFallbackHeuristic(Grounder grounder, WritableAssignment assignment, Random random, HeuristicsConfiguration heuristicsConfiguration) { @@ -163,14 +167,14 @@ protected boolean tryAdvance(Consumer action) { } } - private void initializeSearch() { + protected void initializeSearch() { // Initially, get NoGoods from grounder. performanceLog.initialize(); getNoGoodsFromGrounderAndIngest(); searchState.hasBeenInitialized = true; } - private void prepareForSubsequentAnswerSet() { + protected void prepareForSubsequentAnswerSet() { // We already found one Answer-Set and are requested to find another one. searchState.afterAllAtomsAssigned = false; if (assignment.getDecisionLevel() == 0) { @@ -197,14 +201,14 @@ private void prepareForSubsequentAnswerSet() { } } - private void getNoGoodsFromGrounderAndIngest() { + protected void getNoGoodsFromGrounderAndIngest() { Map obtained = grounder.getNoGoods(assignment); if (!ingest(obtained)) { searchState.isSearchSpaceCompletelyExplored = true; } } - private void learnFromConflict(ConflictCause conflictCause) { + protected void learnFromConflict(ConflictCause conflictCause) { LOGGER.debug("Violating assignment is: {}", assignment); Antecedent conflictAntecedent = conflictCause.getAntecedent(); NoGood violatedNoGood = new NoGood(conflictAntecedent.getReasonLiterals().clone()); @@ -224,7 +228,7 @@ private void learnFromConflict(ConflictCause conflictCause) { } } - private ConflictCause propagate() { + protected ConflictCause propagate() { LOGGER.trace("Doing propagation step."); ConflictCause conflictCause = store.propagate(); LOGGER.trace("Assignment after propagation is: {}", assignment); @@ -236,14 +240,17 @@ private ConflictCause propagate() { } private void provideAnswerSet(Consumer action) { - // NOTE: If we would do optimization, we would now have a guaranteed upper bound. AnswerSet as = translate(assignment.getTrueAssignments()); + if (grounder.inputProgramContainsWeakConstraints()) { + // Adorn AnswerSet with weights if weak constraints are contained in the input program. + as = new WeightedAnswerSet(as, weakConstraintsManager.getCurrentWeightAtLevels()); + } LOGGER.debug("Answer-Set found: {}", as); action.accept(as); logStats(); } - private void backtrackFromMBTsRemaining() { + protected void backtrackFromMBTsRemaining() { LOGGER.debug("Backtracking from wrong choices ({} MBTs).", assignment.getMBTCount()); searchState.afterAllAtomsAssigned = false; if (!justifyMbtAndBacktrack()) { @@ -419,7 +426,7 @@ private boolean treatConflictAfterClosing(Antecedent violatedNoGood) { return true; } - private boolean close() { + protected boolean close() { searchState.afterAllAtomsAssigned = true; return assignment.closeUnassignedAtoms(); } @@ -457,12 +464,9 @@ private boolean backtrack() { return assignment.getDecisionLevel() != 0; } - private boolean ingest(Map obtained) { - assignment.growForMaxAtomId(); - int maxAtomId = atomStore.getMaxAtomId(); - store.growForMaxAtomId(maxAtomId); - choiceManager.growForMaxAtomId(maxAtomId); - branchingHeuristic.growForMaxAtomId(maxAtomId); + protected boolean ingest(Map obtained) { + growForMaxAtomId(); + weakConstraintsManager.addWeakConstraintsInformation(grounder.getWeakConstraintInformation()); branchingHeuristic.newNoGoods(obtained.values()); LinkedList> noGoodsToAdd = new LinkedList<>(obtained.entrySet()); @@ -481,6 +485,14 @@ private boolean ingest(Map obtained) { return true; } + protected void growForMaxAtomId() { + assignment.growForMaxAtomId(); + int maxAtomId = atomStore.getMaxAtomId(); + store.growForMaxAtomId(maxAtomId); + choiceManager.growForMaxAtomId(maxAtomId); + branchingHeuristic.growForMaxAtomId(maxAtomId); + } + /** * Attempts to fix a given conflict that arose from adding a nogood. * @param noGoodEntry the description of the NoGood that caused the conflict. @@ -508,7 +520,7 @@ private boolean fixContradiction(Map.Entry noGoodEntry, Conflic return addAndBackjumpIfNecessary(noGoodEntry.getKey(), noGoodEntry.getValue(), LBD_NO_VALUE); } - private boolean choose() { + protected boolean choose() { choiceManager.addChoiceInformation(grounder.getChoiceAtoms(), grounder.getHeadsToBodies()); choiceManager.updateAssignments(); @@ -524,6 +536,11 @@ private boolean choose() { choiceManager.choose(new Choice(literal, false)); return true; } + + @Override + public boolean didExhaustSearchSpace() { + return searchState.isSearchSpaceCompletelyExplored; + } @Override public int getNumberOfChoices() { @@ -567,7 +584,7 @@ public NoGoodCounter getNoGoodCounter() { return store.getNoGoodCounter(); } - private void logStats() { + protected void logStats() { if (LOGGER.isDebugEnabled()) { LOGGER.debug(getStatisticsString()); if (branchingHeuristic instanceof ChainedBranchingHeuristics) { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveSolver.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveSolver.java index 3da723e59..effd2eb01 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveSolver.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/NaiveSolver.java @@ -27,10 +27,14 @@ */ package at.ac.tuwien.kr.alpha.core.solver; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isNegated; -import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isPositive; -import static java.lang.Math.abs; +import at.ac.tuwien.kr.alpha.api.AnswerSet; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; +import at.ac.tuwien.kr.alpha.core.common.IntIterator; +import at.ac.tuwien.kr.alpha.core.common.NoGood; +import at.ac.tuwien.kr.alpha.core.grounder.Grounder; +import org.apache.commons.lang3.tuple.Pair; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; import java.util.ArrayList; import java.util.HashMap; @@ -41,15 +45,10 @@ import java.util.Stack; import java.util.function.Consumer; -import org.apache.commons.lang3.tuple.Pair; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import at.ac.tuwien.kr.alpha.api.AnswerSet; -import at.ac.tuwien.kr.alpha.core.common.AtomStore; -import at.ac.tuwien.kr.alpha.core.common.IntIterator; -import at.ac.tuwien.kr.alpha.core.common.NoGood; -import at.ac.tuwien.kr.alpha.core.grounder.Grounder; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isNegated; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isPositive; +import static java.lang.Math.abs; /** * Copyright (c) 2016-2020, the Alpha Team. @@ -144,6 +143,13 @@ protected boolean tryAdvance(Consumer action) { } } + + @Override + public boolean didExhaustSearchSpace() { + // Note: private method NaiveSolver::didExhaustSearchSpace assumes being called only after the first choice and does not work here. + throw new UnsupportedOperationException("NaiveSolver cannot report whether search space was exhausted."); + } + private void assignUnassignedToFalse() { for (Integer atom : unassignedAtoms) { truthAssignments.put(atom, false); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/OptimizingSolver.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/OptimizingSolver.java new file mode 100644 index 000000000..2710a515d --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/OptimizingSolver.java @@ -0,0 +1,91 @@ +package at.ac.tuwien.kr.alpha.core.solver; + +import at.ac.tuwien.kr.alpha.api.AnswerSet; +import at.ac.tuwien.kr.alpha.core.common.AtomStore; +import at.ac.tuwien.kr.alpha.core.common.NoGood; +import at.ac.tuwien.kr.alpha.commons.WeightedAnswerSet; +import at.ac.tuwien.kr.alpha.api.config.SystemConfig; +import at.ac.tuwien.kr.alpha.core.grounder.Grounder; +import at.ac.tuwien.kr.alpha.core.solver.heuristics.HeuristicsConfiguration; +import at.ac.tuwien.kr.alpha.core.solver.optimization.WeakConstraintsManagerForBoundedOptimality; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.LinkedHashMap; +import java.util.Map; +import java.util.Random; +import java.util.function.Consumer; + +/** + * A solver providing optimization via weak constraints and a simpla branch-and-bound algorithm. + * The basis of this solver is the {@link DefaultSolver} and its algorithms. + * + * Copyright (c) 2021, the Alpha Team. + */ +public class OptimizingSolver extends DefaultSolver { + private static final Logger LOGGER = LoggerFactory.getLogger(OptimizingSolver.class); + + public OptimizingSolver(AtomStore atomStore, Grounder grounder, NoGoodStore store, WritableAssignment assignment, Random random, SystemConfig config, HeuristicsConfiguration heuristicsConfiguration) { + super(atomStore, grounder, store, assignment, random, config, heuristicsConfiguration); + this.weakConstraintsManager = new WeakConstraintsManagerForBoundedOptimality(assignment, config.getAnswerSetsMaxWeightAtLevels()); + this.weakConstraintsManager.setChecksEnabled(config.isDebugInternalChecks()); + } + + @Override + protected boolean tryAdvance(Consumer action) { + if (!searchState.hasBeenInitialized) { + initializeSearch(); + } else { + prepareForSubsequentAnswerSet(); + } + // Try all assignments until grounder reports no more NoGoods and all of them are satisfied + while (true) { + performanceLog.writeIfTimeForLogging(LOGGER); + if (searchState.isSearchSpaceCompletelyExplored) { + LOGGER.debug("Search space has been fully explored, there are no more answer-sets."); + logStats(); + return false; + } + ConflictCause conflictCause = propagate(); + if (conflictCause != null) { + LOGGER.debug("Conflict encountered, analyzing conflict."); + learnFromConflict(conflictCause); + } else if (!((WeakConstraintsManagerForBoundedOptimality)weakConstraintsManager).isCurrentBetterThanBest()) { + LOGGER.debug("Current assignment is worse than previously found answer set, backjumping now."); + backtrackFromBound(); + } else if (assignment.didChange()) { + LOGGER.debug("Updating grounder with new assignments and (potentially) obtaining new NoGoods."); + grounder.updateAssignment(assignment.getNewPositiveAssignmentsIterator()); + getNoGoodsFromGrounderAndIngest(); + } else if (choose()) { + LOGGER.debug("Did choice."); + } else if (close()) { + LOGGER.debug("Closed unassigned known atoms (assigning FALSE)."); + } else if (assignment.getMBTCount() == 0) { + provideAnswerSet(action); + return true; + } else { + backtrackFromMBTsRemaining(); + } + } + } + + private void backtrackFromBound() { + NoGood excludingNoGood = ((WeakConstraintsManagerForBoundedOptimality)weakConstraintsManager).generateExcludingNoGood(); + Map obtained = new LinkedHashMap<>(); + obtained.put(grounder.register(excludingNoGood), excludingNoGood); + if (!ingest(obtained)) { + searchState.isSearchSpaceCompletelyExplored = true; + } + } + + private void provideAnswerSet(Consumer action) { + // Enrich answer-set with weights information and record current-best upper bound. + AnswerSet as = translate(assignment.getTrueAssignments()); + ((WeakConstraintsManagerForBoundedOptimality)weakConstraintsManager).markCurrentWeightAsBestKnown(); + WeightedAnswerSet was = new WeightedAnswerSet(as, weakConstraintsManager.getCurrentWeightAtLevels()); + LOGGER.debug("Answer-Set found: {}", was); + action.accept(was); + logStats(); + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java index e6af12d0a..118770e92 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/SolverFactory.java @@ -63,7 +63,11 @@ public static Solver getInstance(SystemConfig config, AtomStore atomStore, Groun case "naive" : return new NaiveSolver(atomStore, grounder); case "default": - return new DefaultSolver(atomStore, grounder, store, assignment, random, config, heuristicsConfiguration); + if (config.isAnswerSetOptimizationEnabled()) { + return new OptimizingSolver(atomStore, grounder, store, assignment, random, config, heuristicsConfiguration); + } else { + return new DefaultSolver(atomStore, grounder, store, assignment, random, config, heuristicsConfiguration); + } } throw new IllegalArgumentException("Unknown solver requested."); } diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java index ed7e4b1fb..9f483e367 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/TrailAssignment.java @@ -81,7 +81,7 @@ public String toString() { }; private final AtomStore atomStore; - private ChoiceManager choiceManagerCallback; + private AtomCallbackManager atomCallbackManager = new AtomCallbackManager(); /** * Contains for each known atom a value whose two least @@ -146,8 +146,8 @@ public void registerCallbackOnChange(int atom) { } @Override - public void setCallback(ChoiceManager choiceManager) { - choiceManagerCallback = choiceManager; + public AtomCallbackManager getAtomCallbackManager() { + return atomCallbackManager; } @Override @@ -211,7 +211,7 @@ int getOutOfOrderStrongDecisionLevel(int atom) { private void informCallback(int atom) { if (callbackUponChange[atom]) { - choiceManagerCallback.callbackOnChanged(atom); + atomCallbackManager.callbackOnChanged(atom); } } @@ -563,6 +563,7 @@ public void growForMaxAtomId() { impliedBy = Arrays.copyOf(impliedBy, newCapacity); callbackUponChange = Arrays.copyOf(callbackUponChange, newCapacity); trail = Arrays.copyOf(trail, newCapacity * 2); // Trail has at most 2 assignments (MBT+TRUE) for each atom. + atomCallbackManager.growForMaxAtomId(maxAtomId); } public int getNumberOfAssignedAtoms() { diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/WritableAssignment.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/WritableAssignment.java index f17d76277..f501f82ec 100644 --- a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/WritableAssignment.java +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/WritableAssignment.java @@ -74,7 +74,7 @@ default ConflictCause assign(int atom, ThriceTruth value) { void registerCallbackOnChange(int atom); - void setCallback(ChoiceManager choiceManager); + AtomCallbackManager getAtomCallbackManager(); default ConflictCause choose(int atom, boolean value) { return choose(atom, ThriceTruth.valueOf(value)); diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintAtomCallback.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintAtomCallback.java new file mode 100644 index 000000000..6d33198e1 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintAtomCallback.java @@ -0,0 +1,55 @@ +package at.ac.tuwien.kr.alpha.core.solver.optimization; + +import at.ac.tuwien.kr.alpha.core.solver.AtomCallbackManager; +import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; + +import java.util.Objects; + +/** + * Atom callbacks for weak constraints. + * + * Copyright (c) 2021, the Alpha Team. + */ +public class WeakConstraintAtomCallback implements AtomCallbackManager.AtomCallback { + private final WeakConstraintsManagerForBoundedOptimality weakConstraintsManagerForBoundedOptimality; + public final int atom; + public final int weight; + public final int level; + public ThriceTruth lastTruthValue; + + WeakConstraintAtomCallback(WeakConstraintsManagerForBoundedOptimality weakConstraintsManager, int atom, int weight, int level) { + this.atom = atom; + this.weight = weight; + this.level = level; + this.weakConstraintsManagerForBoundedOptimality = weakConstraintsManager; + } + + @Override + public void processCallback() { + weakConstraintsManagerForBoundedOptimality.processCallback(this); + } + + @Override + public boolean equals(Object o) { + if (this == o) { + return true; + } + if (o == null || getClass() != o.getClass()) { + return false; + } + WeakConstraintAtomCallback that = (WeakConstraintAtomCallback) o; + return atom == that.atom && + weight == that.weight && + level == that.level; + } + + @Override + public int hashCode() { + return Objects.hash(atom, weight, level); + } + + @Override + public String toString() { + return atom + "[" + weight + "@" + level + "]=" + lastTruthValue; + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManager.java new file mode 100644 index 000000000..7110d3c81 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManager.java @@ -0,0 +1,28 @@ +package at.ac.tuwien.kr.alpha.core.solver.optimization; + +import at.ac.tuwien.kr.alpha.core.solver.Checkable; +import org.apache.commons.lang3.tuple.Triple; + +import java.util.List; +import java.util.TreeMap; + +/** + * A {@link WeakConstraintsManager} enables the solver to compute the valuation of answer-sets if weak constraints are + * present in the input program. + * Copyright (c) 2023, the Alpha Team. + */ +public interface WeakConstraintsManager extends Checkable { + + /** + * Registers newly obtained weak constraint atoms to be respected by the {@link WeakConstraintsManager}. + * @param weakConstraintAtomWeightLevels a list of triples (a,b,c) representing weak constraint atoms, where a is + * the atom, b the weight and c the level of the respective weak constraint. + */ + void addWeakConstraintsInformation(List> weakConstraintAtomWeightLevels); + + /** + * Returns the valuation of the current assignment as weights and their levels. + * @return a TreeMap mapping levels to weight, only levels with weight != 0 are guaranteed to be reported. + */ + TreeMap getCurrentWeightAtLevels(); +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManagerForBoundedOptimality.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManagerForBoundedOptimality.java new file mode 100644 index 000000000..0072e1308 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManagerForBoundedOptimality.java @@ -0,0 +1,231 @@ +package at.ac.tuwien.kr.alpha.core.solver.optimization; + +import at.ac.tuwien.kr.alpha.core.common.NoGood; +import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth; +import at.ac.tuwien.kr.alpha.core.solver.WritableAssignment; +import org.apache.commons.lang3.tuple.Triple; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.TreeMap; +import java.util.stream.Collectors; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; +import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomToLiteral; +import static at.ac.tuwien.kr.alpha.core.solver.ThriceTruth.MBT; + +/** + * Manages weak constraints: stores the value of the current partial assignment, the best known value of any answer-set, + * and handles callbacks/computations when certain atoms (that represent weak constraints) change their truth value. + * + * Copyright (c) 2020-2021, the Alpha Team. + */ +public class WeakConstraintsManagerForBoundedOptimality implements WeakConstraintsManager { + private static final Logger LOGGER = LoggerFactory.getLogger(WeakConstraintsManagerForBoundedOptimality.class); + + final WritableAssignment assignment; + final WeightAtLevelsManager weightAtLevelsManager; + private final ArrayList knownCallbackAtoms; + private final ArrayList knownAtomCallbacksForFirstAnswerSet = new ArrayList<>(); + private boolean foundFirstAnswerSet; + private final HashSet aboveMaxLevelTrueAtoms = new HashSet<>(); + + public WeakConstraintsManagerForBoundedOptimality(WritableAssignment assignment, String answerSetsMaxWeightAtLevels) { + this.assignment = assignment; + if (answerSetsMaxWeightAtLevels.isEmpty()) { + this.weightAtLevelsManager = new WeightAtLevelsManager(); + } else { + // If maximum weights are given, initialize accordingly and consider it as an already found answer-set. + this.weightAtLevelsManager = new WeightAtLevelsManager(answerSetsMaxWeightAtLevels); + this.foundFirstAnswerSet = true; + } + this.knownCallbackAtoms = new ArrayList<>(); + } + + /** + * Registers newly obtained weak constraint atoms for callback at the assignment. + * @param weakConstraintAtomWeightLevels a set of triples (a,b,c) representing weak constraint atoms, where a is + * the atom, b the weight and c the level of the respective weak constraint. + */ + @Override + public void addWeakConstraintsInformation(List> weakConstraintAtomWeightLevels) { + for (Triple weakConstraintAtomWeightLevel : weakConstraintAtomWeightLevels) { + if (weakConstraintAtomWeightLevel.getMiddle() == 0) { + // Skip weak constraints with weight 0 entirely. + continue; + } + WeakConstraintAtomCallback wcA = new WeakConstraintAtomCallback(this, weakConstraintAtomWeightLevel.getLeft(), weakConstraintAtomWeightLevel.getMiddle(), weakConstraintAtomWeightLevel.getRight()); + assignment.registerCallbackOnChange(wcA.atom); + assignment.getAtomCallbackManager().recordCallback(wcA.atom, wcA); + knownCallbackAtoms.add(wcA.atom); + if (assignment.getTruth(wcA.atom) != null) { + throw oops("Adding weak constraints information and atom callback already has a truth value assigned."); + } + if (!foundFirstAnswerSet) { + knownAtomCallbacksForFirstAnswerSet.add(wcA); + } + } + } + + /** + * Process the the changed truth value of an atom representing a weak constraint. + * + * @param atomCallback the {@link WeakConstraintAtomCallback} whose assigned truth value did change. + */ + public void processCallback(WeakConstraintAtomCallback atomCallback) { + final int atom = atomCallback.atom; + final int level = atomCallback.level; + final int weight = atomCallback.weight; + ThriceTruth lastTruthValue = atomCallback.lastTruthValue; + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Processing callback for atom {} with weight at level {}@{}, last truth value was {}.", atom, weight, level, lastTruthValue); + LOGGER.trace("Current atom truth value is: {}", assignment.getTruth(atom)); + } + ThriceTruth currentAtomTruth = assignment.getTruth(atom); + if (!foundFirstAnswerSet) { + // Record old truth value and return if no answer set has been found yet. + atomCallback.lastTruthValue = currentAtomTruth; + LOGGER.trace("End processing callback as no first answer set has been found."); + return; + } + LOGGER.trace("Current truth value is: {}", currentAtomTruth); + atomCallback.lastTruthValue = currentAtomTruth; + if (lastTruthValue == null) { + // Change from unassigned to some truth value. + if (currentAtomTruth == MBT) { + increaseWeight(atomCallback); + } + // Note: for assignment to FALSE or MBT->TRUE, no change needed. + } else { + // Decrease if change from TRUE/MBT to unassigned. + if (lastTruthValue.toBoolean() && currentAtomTruth == null) { + decreaseWeight(atomCallback); + } + // Note: for backtracking from TRUE to MBT no change is needed. + if (currentAtomTruth != null && lastTruthValue.toBoolean() && !currentAtomTruth.toBoolean()) { + throw oops("Unexpected case of weak constraint atom directly changing truth value from MBT/TRUE to FALSE encountered. Atom/LastTruth/CurrentTruth: " + atom + "/" + lastTruthValue + "/" + currentAtomTruth); + } + } + LOGGER.trace("End Processing callback for atom {} with weight at level {}@{}, last truth value was {}, current is {}.", atom, weight, level, lastTruthValue, currentAtomTruth); + } + + private void increaseWeight(WeakConstraintAtomCallback atomCallback) { + if (weightAtLevelsManager.getMaxLevel() < atomCallback.level) { + LOGGER.trace("Adding higher level than possible with weightAtLevelsManager: level={} and maxLevel={}, callback is: {}.", atomCallback.level, weightAtLevelsManager.getMaxLevel(), atomCallback); + aboveMaxLevelTrueAtoms.add(atomCallback); + } else { + weightAtLevelsManager.increaseCurrentWeight(atomCallback.level, atomCallback.weight); + } + } + + private void decreaseWeight(WeakConstraintAtomCallback atomCallback) { + if (weightAtLevelsManager.getMaxLevel() < atomCallback.level) { + LOGGER.trace("Removing higher level than possible with weightAtLevelsManager: level={} and maxLevel={}, callback is: {}.", atomCallback.level, weightAtLevelsManager.getMaxLevel(), atomCallback); + aboveMaxLevelTrueAtoms.remove(atomCallback); + } else { + weightAtLevelsManager.decreaseCurrentWeight(atomCallback.level, atomCallback.weight); + } + } + + /** + * Returns whether the current partial interpretation is already worse (or equal) than the best-known answer-set. + * @return true if the current partial interpretation has worse (or equal) weight than the best-known answer-set. + */ + public boolean isCurrentBetterThanBest() { + if (!foundFirstAnswerSet) { + return true; + } + boolean isCurrentBetterThanBest = aboveMaxLevelTrueAtoms.isEmpty() && weightAtLevelsManager.isCurrentBetterThanBest(); + LOGGER.trace("Is current better than best? {}", isCurrentBetterThanBest); + return isCurrentBetterThanBest; + } + + /** + * Mark the current weight as being the best of all currently known answer-sets. + */ + public void markCurrentWeightAsBestKnown() { + if (!foundFirstAnswerSet) { + initializeFirstWeightsAtLevel(); + foundFirstAnswerSet = true; + } else { + if (!isCurrentBetterThanBest()) { + throw oops("WeakConstraintsManager instructed to mark current valuation as best-known, but there is a better one already."); + } + } + if (!aboveMaxLevelTrueAtoms.isEmpty()) { + throw oops("WeakConstraintsManager has aboveMaxLevelTrueAtoms but is called to markCurrentWeightsAsBestKnown."); + } + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + } + + private void initializeFirstWeightsAtLevel() { + // First answer set has been found, find its maximum level and inform WeightAtLevelsManager. + LOGGER.trace("Initializing for first answer-set."); + int highestLevel = 0; + List trueWeakConstraintAtomCallbacks = knownAtomCallbacksForFirstAnswerSet + .stream() + .filter(wca -> assignment.getTruth(wca.atom).toBoolean()) + .collect(Collectors.toList()); + for (WeakConstraintAtomCallback weakConstraintAtomCallback : trueWeakConstraintAtomCallbacks) { + int level = weakConstraintAtomCallback.level; + if (highestLevel < level) { + highestLevel = level; + } + } + weightAtLevelsManager.setMaxLevel(highestLevel); + // Now inform WeightAtLevelsManager about all true weak constraint atoms. + for (WeakConstraintAtomCallback weakConstraintAtomCallback : trueWeakConstraintAtomCallbacks) { + weightAtLevelsManager.increaseCurrentWeight(weakConstraintAtomCallback.level, weakConstraintAtomCallback.weight); + } + } + + /** + * Generates a NoGood that prevents the current weight to be derived again. + * @return a NoGood which excludes the exact weight of the current assignment. + */ + public NoGood generateExcludingNoGood() { + LOGGER.trace("Generating excluding NoGood."); + // Collect all currently true/mbt weights and put their respective literals in one nogood. + // Note: alternative to searching all known callback atoms would be maintaining a list of true ones, but this is probably less efficient. + ArrayList trueCallbackAtoms = new ArrayList<>(); + for (Integer callbackAtom : knownCallbackAtoms) { + ThriceTruth truth = assignment.getTruth(callbackAtom); + if (truth != null && truth.toBoolean()) { + trueCallbackAtoms.add(atomToLiteral(callbackAtom)); + } + } + LOGGER.trace("True weak constraint representing atoms are: {}", trueCallbackAtoms); + return NoGood.fromConstraint(trueCallbackAtoms, Collections.emptyList()); + } + + @Override + public void setChecksEnabled(boolean checksEnabled) { + weightAtLevelsManager.setChecksEnabled(checksEnabled); + } + + /** + * Returns the current weights and their levels. + * @return a TreeMap mapping levels to weights. + */ + @Override + public TreeMap getCurrentWeightAtLevels() { + LOGGER.trace("Reporting current weight at levels."); + TreeMap weightAtLevels = weightAtLevelsManager.getCurrentWeightAtLevels(); + if (aboveMaxLevelTrueAtoms.isEmpty()) { + LOGGER.trace("Current weight at levels: {}", weightAtLevels); + return weightAtLevels; + } + // Add weights above the maximum level stored in the WeightAtLevelsManager. + for (WeakConstraintAtomCallback aboveMaxLevelTrueAtom : aboveMaxLevelTrueAtoms) { + Integer weightAtLevel = weightAtLevels.get(aboveMaxLevelTrueAtom.level); + weightAtLevel = weightAtLevel == null ? 0 : weightAtLevel; + weightAtLevels.putIfAbsent(aboveMaxLevelTrueAtom.level, weightAtLevel + aboveMaxLevelTrueAtom.weight); + } + LOGGER.trace("Current weight at levels: {}", weightAtLevels); + return weightAtLevels; + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManagerForUnboundedEnumeration.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManagerForUnboundedEnumeration.java new file mode 100644 index 000000000..b822deb6c --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeakConstraintsManagerForUnboundedEnumeration.java @@ -0,0 +1,52 @@ +package at.ac.tuwien.kr.alpha.core.solver.optimization; + +import at.ac.tuwien.kr.alpha.core.solver.WritableAssignment; +import org.apache.commons.lang3.tuple.Triple; + +import java.util.ArrayList; +import java.util.List; +import java.util.TreeMap; + +/** + * Enables the valuation of an answer-set based on weak constraints. + * This implementation is not based on callbacks whenever atoms change their assignment but rather checks all + * {@link at.ac.tuwien.kr.alpha.grounder.atoms.WeakConstraintAtom}s sequentially whenever a valuation is requested. + * This implementation is intended to provide valuations only for full answer-sets. + * Copyright (c) 2023, the Alpha Team. + */ +public class WeakConstraintsManagerForUnboundedEnumeration implements WeakConstraintsManager { + + private final List> knownAtomValuations = new ArrayList<>(); + private final WritableAssignment assignment; + + public WeakConstraintsManagerForUnboundedEnumeration(WritableAssignment assignment) { + this.assignment = assignment; + } + + @Override + public void setChecksEnabled(boolean checksEnabled) { + + } + + @Override + public void addWeakConstraintsInformation(List> weakConstraintAtomWeightLevels) { + knownAtomValuations.addAll(weakConstraintAtomWeightLevels); + } + + @Override + public TreeMap getCurrentWeightAtLevels() { + TreeMap currentWeights = new TreeMap<>(); + for (Triple atomWeightLevel : knownAtomValuations) { + if (assignment.getTruth(atomWeightLevel.getLeft()).toBoolean()) { + Integer atomLevel = atomWeightLevel.getRight(); + Integer currentWeight = currentWeights.get(atomLevel); + if (currentWeight == null) { + currentWeights.put(atomLevel, atomWeightLevel.getMiddle()); + } else { + currentWeights.put(atomLevel, currentWeight + atomWeightLevel.getMiddle()); + } + } + } + return currentWeights; + } +} diff --git a/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeightAtLevelsManager.java b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeightAtLevelsManager.java new file mode 100644 index 000000000..2d619c5d9 --- /dev/null +++ b/alpha-core/src/main/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeightAtLevelsManager.java @@ -0,0 +1,372 @@ +package at.ac.tuwien.kr.alpha.core.solver.optimization; + +import at.ac.tuwien.kr.alpha.commons.WeightedAnswerSet; +import at.ac.tuwien.kr.alpha.core.solver.Checkable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.ArrayList; +import java.util.Map; +import java.util.TreeMap; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.oops; +import static java.lang.Math.max; + +/** + * Manages two sets of weights-at-levels (basically the valuation of two potential answer-sets). One set is the + * valuation of the best-known answer-set at the time, the other is the (partial) valuation of the currently explored + * (partial) answer-set. + * + * Weights-at-levels are stored in arrays in reverse order (array position 0 is most important level). Therefore, the + * maximum level must be declared upfront. Furthermore, the array may grow if less-important levels are added later and + * it is automatically trimmed if highest-level weights are 0 when marking the current valuation as the best-known one. + * + * Code using this class must therefore ensure not to add weights at levels beyond the current maximum one. + * + * Copyright (c) 2021, the Alpha Team. + */ +public class WeightAtLevelsManager implements Checkable { + private static final Logger LOGGER = LoggerFactory.getLogger(WeightAtLevelsManager.class); + private boolean checksEnabled; + + // Stores weights in inverted order: zero is highest violated level, may also grow to represent negative levels. + private ArrayList currentWeightAtLevels; + private ArrayList bestKnownWeightAtLevels; + // The highest level for which holds: on all levels below (or equal), the current weights are the same as the weights for the best known. + private int maxOffsetCurrentIsAllEqualBest; + // Stores which actual level corresponds to array position 0 in bestKnownWeightAtLevels, i.e, the highest level that is violated. Value may decrease if better answer-sets are found. + private int maxLevel; + private boolean isCurrentBetterThanBest; + private boolean hasBestKnown; + + public WeightAtLevelsManager() { + bestKnownWeightAtLevels = new ArrayList<>(); + maxOffsetCurrentIsAllEqualBest = -1; + isCurrentBetterThanBest = true; + } + + /** + * Initializes {@link WeightAtLevelsManager} with given upper bound, i.e., bound is taken valuation of a best-known answer-set. + * @param maximumWeightAtLevels a comma-separated list of weight@levels pairs. + */ + public WeightAtLevelsManager(String maximumWeightAtLevels) { + this(); + if (maximumWeightAtLevels.isEmpty()) { + throw new IllegalArgumentException("Initial maximum bound is empty."); + } + initializeFromString(maximumWeightAtLevels); + } + + private void initializeFromString(String maximumWeightAtLevels) { + TreeMap levelsToWeight = WeightedAnswerSet.weightPerLevelFromString(maximumWeightAtLevels); + int maxLevel = 0; + for (Map.Entry levelAndWeight : levelsToWeight.entrySet()) { + if (levelAndWeight.getKey() > maxLevel && levelAndWeight.getValue() > 0) { + maxLevel = levelAndWeight.getKey(); + } + } + // Initialize according to parsed weights at levels. + setMaxLevel(maxLevel); + for (Map.Entry levelToWeight : levelsToWeight.entrySet()) { + increaseCurrentWeight(levelToWeight.getKey(), levelToWeight.getValue()); + } + markCurrentWeightAsBestKnown(); + // Re-set the current weight at all levels back to zero. + for (Map.Entry levelToWeight : levelsToWeight.entrySet()) { + decreaseCurrentWeight(levelToWeight.getKey(), levelToWeight.getValue()); + } + } + + @Override + public void setChecksEnabled(boolean checksEnabled) { + this.checksEnabled = checksEnabled; + } + + /** + * Returns whether the current valuation is (still) better than the best-known one. + * @return true iff the current weights-at-levels are better than the best-known. + */ + public boolean isCurrentBetterThanBest() { + if (checksEnabled) { + runChecks(); + } + if (!hasBestKnown) { + throw oops("WeightAtLevelsManager has no best-known valuation yet."); + } + return isCurrentBetterThanBest; + } + + /** + * Returns the current weights and their levels. + * @return a TreeMap mapping levels to weights. Note that values may be non-continuous and negative levels are possible. + */ + public TreeMap getCurrentWeightAtLevels() { + TreeMap weightPerLevels = new TreeMap<>(); + for (int i = 0; i < currentWeightAtLevels.size(); i++) { + Integer weightAti = currentWeightAtLevels.get(i); + if (weightAti == 0) { + continue; + } + weightPerLevels.put(listOffsetToLevel(i), weightAti); + } + return weightPerLevels; + } + + /** + * Returns the current maximum level. Note that this may be smaller than a previously set one as the maximum + * level may decrease following the marking of another valuation as best-known. + * @return the current maximum level. + */ + public int getMaxLevel() { + return maxLevel; + } + + /** + * Increases the current valuation at the given level by the given weight. + * @param level the level to increase. + * @param weight the weight at the level. + */ + public void increaseCurrentWeight(int level, int weight) { + if (checksEnabled) { + runChecks(); + } + if (level > maxLevel) { + throw oops("WeightAtLevelsManager invoked to increase violation above maximum declared level."); + } + // Record the new weight. + growForLevel(currentWeightAtLevels, level); + int listOffset = levelToListOffset(level); + int newWeight = currentWeightAtLevels.get(listOffset) + weight; + currentWeightAtLevels.set(listOffset, newWeight); + + // Now check whether current is worse than best known. + if (listOffset > maxOffsetCurrentIsAllEqualBest + 1) { + // Weight in some level where differences do not (yet) matter increased, but on lower level current partial assignment is still better than best found answer-set. + // Nothing to do here. + return; + } else if (listOffset <= maxOffsetCurrentIsAllEqualBest) { + // Weight in level with previously equal weights increased, current is now worse than best. + isCurrentBetterThanBest = false; + maxOffsetCurrentIsAllEqualBest = listOffset - 1; + } else if (listOffset == maxOffsetCurrentIsAllEqualBest + 1) { + // Weight increased for the first level where current and best-known are not equal. + moveUpwardsMaxOffsetCurrentIsAllEqual(); + recomputeIsCurrentBetterThanBest(); + } else { + throw oops("Increasing weight of current answer reached unforeseen state."); + } + if (checksEnabled) { + runChecks(); + } + } + + /** + * Decreases the current valuation at the given level by the given weight. + * @param level the level to decrease. + * @param weight the weight at the level. + */ + public void decreaseCurrentWeight(int level, int weight) { + if (checksEnabled) { + runChecks(); + } + if (level > maxLevel) { + throw oops("WeightAtLevelsManager invoked to decrease violation above maximum declared level."); + } + // Record the new weight. + int listOffset = levelToListOffset(level); + int newWeight = currentWeightAtLevels.get(listOffset) - weight; + currentWeightAtLevels.set(listOffset, newWeight); + + // Now check whether current is better than best known and adapt maxOffsetCurrentIsAllEqualBest. + if (listOffset <= maxOffsetCurrentIsAllEqualBest) { + // Improved below the point where current is equal to best, so current is better than best now. + isCurrentBetterThanBest = true; + // All weights below the change are equal. + maxOffsetCurrentIsAllEqualBest = listOffset - 1; + } else if (listOffset > maxOffsetCurrentIsAllEqualBest + 1) { + // Decrease in such a high level, that there is at least one level (maxLevel+1) where weights are + // different and whose difference still dominates whether current is better than best known. + return; + } else if (listOffset == maxOffsetCurrentIsAllEqualBest + 1) { + // Decrease might make current better than best known and change level of equals. + moveUpwardsMaxOffsetCurrentIsAllEqual(); + recomputeIsCurrentBetterThanBest(); + } else { + throw oops("Decreasing weight of current answer reached unforeseen state."); + } + if (checksEnabled) { + runChecks(); + } + } + + private void moveUpwardsMaxOffsetCurrentIsAllEqual() { + for (int i = max(maxOffsetCurrentIsAllEqualBest, 0); i < currentWeightAtLevels.size(); i++) { + int currentLevelWeight = currentWeightAtLevels.get(i); + int bestLevelWeight = bestKnownWeightAtLevels.size() > i ? bestKnownWeightAtLevels.get(i) : 0; + if (currentLevelWeight != bestLevelWeight) { + // Level is the first where values differ, previous level was maximum one where values are equal. + maxOffsetCurrentIsAllEqualBest = i - 1; + return; + } + } + // Iterated all levels, so weights are the same on all levels. + maxOffsetCurrentIsAllEqualBest = currentWeightAtLevels.size() - 1; + } + + private void recomputeIsCurrentBetterThanBest() { + // The weights at the first level above maxOffsetCurrentIsAllEqualBest dominate whether current is worse than best known. + if (maxOffsetCurrentIsAllEqualBest == currentWeightAtLevels.size() - 1) { + // Current and best known are equal even up to the last level. + isCurrentBetterThanBest = false; + return; + } + int comparisonOffset = maxOffsetCurrentIsAllEqualBest + 1; + int currentLevelWeight = currentWeightAtLevels.get(comparisonOffset); + int bestLevelWeight = bestKnownWeightAtLevels.size() > comparisonOffset ? bestKnownWeightAtLevels.get(comparisonOffset) : 0; + isCurrentBetterThanBest = currentLevelWeight < bestLevelWeight; + } + + private int listOffsetToLevel(int offset) { + return maxLevel - offset; + } + + private void growForLevel(ArrayList listToGrow, int level) { + int listOffset = levelToListOffset(level); + while (listOffset >= listToGrow.size()) { + listToGrow.add(0); + } + } + + /** + * Marks the current valuation/weights-at-levels as being the best-known one. + * + * May shrink the underlying maximum level if current highest level(s) are zero. + */ + public void markCurrentWeightAsBestKnown() { + LOGGER.trace("Marking current answer-set as best known."); + if (!hasBestKnown) { + hasBestKnown = true; + LOGGER.trace(" Initially, current/best known weights are: {}", currentWeightAtLevels); + } + trimZeroWeightLevels(); + bestKnownWeightAtLevels = new ArrayList<>(currentWeightAtLevels); + maxOffsetCurrentIsAllEqualBest = bestKnownWeightAtLevels.size() - 1; + LOGGER.trace(" Max offset current is all equal to best known is: {}", maxOffsetCurrentIsAllEqualBest); + LOGGER.trace(" Current/Best known weights are: {}", bestKnownWeightAtLevels); + isCurrentBetterThanBest = false; + LOGGER.trace("End marking current answer-set as best known."); + } + + /** + * Removes unnecessary high levels (with weights 0) from current valuation. + */ + private void trimZeroWeightLevels() { + int trim = 0; + for (int i = 0; i < currentWeightAtLevels.size(); i++) { + if (currentWeightAtLevels.get(i) != 0) { + trim = i; + break; + } + } + if (trim > 0) { + currentWeightAtLevels = new ArrayList<>(currentWeightAtLevels.subList(trim, currentWeightAtLevels.size())); + maxLevel -= trim; + } + } + + /** + * Initializes the maximum level that will ever be encountered while solving. + * This method may only be called once and must be called before the first weights are set/increased. + * + * Note that the maximum level may decrease automatically following calls to markCurrentWeightAsBestKnown. + * + * @param maxLevel the highest level ever to be encountered. + */ + public void setMaxLevel(int maxLevel) { + if (currentWeightAtLevels != null) { + throw oops("WeightAtLevelsManager.setMaxLevel called more than once."); + } + this.maxLevel = maxLevel; + LOGGER.trace("Maximum level (0-offset) is set to: {} ({})", maxLevel, listOffsetToLevel(0)); + currentWeightAtLevels = new ArrayList<>(); + } + + private int levelToListOffset(int level) { + int levelInList = maxLevel - level; + if (levelInList < 0) { + throw oops("Level optimisation in WeightAtLevelsManager is negative."); + } + return levelInList; + } + + private void runChecks() { + if (LOGGER.isTraceEnabled()) { + LOGGER.trace("Running checks."); + LOGGER.trace("Maximum recorded level (0-offset) is: {} ({})", maxLevel, listOffsetToLevel(0)); + LOGGER.trace("Currently best known weights are: {}", bestKnownWeightAtLevels); + LOGGER.trace("Current weights are: {}", currentWeightAtLevels); + LOGGER.trace("Max offset current is all equal to best known is: {}", maxOffsetCurrentIsAllEqualBest); + LOGGER.trace("Is current better than best-known: {}", isCurrentBetterThanBest); + + } + if (!hasBestKnown && !bestKnownWeightAtLevels.isEmpty()) { + throw oops("WeightAtLevelsManager has best known answer set information but no answer set was found yet."); + } + checkBestKnownFreeOfLeadingZeroLevels(); + if (hasBestKnown) { + // Check whether isCurrentBetterThanBest flag is consistent. + if (isCurrentBetterThanBest != checkIsCurrentBetterThanBest()) { + throw oops("WeightAtLevelsManager detected valuation of current assignment is inconsistent with state flag."); + } + checkLevelBar(); + } + LOGGER.trace("Checks done."); + } + + private void checkBestKnownFreeOfLeadingZeroLevels() { + // Tolerate Zero weight if there is only one level. + if (!hasBestKnown || bestKnownWeightAtLevels.size() == 1) { + return; + } + if (!bestKnownWeightAtLevels.isEmpty() && bestKnownWeightAtLevels.get(0) == 0) { + throw oops("WeightAtLevelsManager has best-known answer set with zero-weights at highest level."); + } + } + + private void checkLevelBar() { + int highestLevelWhereLowerLevelsAreEqual = -1; + for (int i = 0; i < currentWeightAtLevels.size(); i++) { + int levelValue = i < bestKnownWeightAtLevels.size() ? bestKnownWeightAtLevels.get(i) : 0; + if (currentWeightAtLevels.get(i) != levelValue) { + break; + } + highestLevelWhereLowerLevelsAreEqual = i; + } + // The level bar should be at highestLevelWhereLowerLevelsAreEqual+1. + if (maxOffsetCurrentIsAllEqualBest != highestLevelWhereLowerLevelsAreEqual) { + throw oops("WeightAtLevelsManager detected level bar at wrong level, it is " + maxOffsetCurrentIsAllEqualBest + + "and should be " + highestLevelWhereLowerLevelsAreEqual); + } + } + + private boolean checkIsCurrentBetterThanBest() { + if (!hasBestKnown) { + // If no answer set has been found, the current is always better than best known. + return true; + } + for (int i = 0; i < currentWeightAtLevels.size(); i++) { + if (i >= bestKnownWeightAtLevels.size()) { + // Current has violations at level not violated by best. + return false; + } + if (currentWeightAtLevels.get(i) < bestKnownWeightAtLevels.get(i)) { + return true; + } + if (currentWeightAtLevels.get(i) > bestKnownWeightAtLevels.get(i)) { + return false; + } + } + // All levels have same weight for current as for best known, so at this point usually current is not better than best. + return false; + } +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java index 530d54944..fbd409064 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/ChoiceGrounder.java @@ -27,25 +27,6 @@ */ package at.ac.tuwien.kr.alpha.core.grounder; -import static at.ac.tuwien.kr.alpha.commons.util.Util.entriesToMap; -import static at.ac.tuwien.kr.alpha.commons.util.Util.entry; -import static at.ac.tuwien.kr.alpha.core.common.NoGood.headFirst; -import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals; -import static java.util.Arrays.asList; - -import java.util.Arrays; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Map; -import java.util.Set; -import java.util.SortedSet; -import java.util.TreeSet; -import java.util.stream.Stream; - -import org.apache.commons.lang3.tuple.ImmutablePair; -import org.apache.commons.lang3.tuple.Pair; - import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.programs.Predicate; import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom; @@ -66,6 +47,27 @@ import at.ac.tuwien.kr.alpha.core.programs.atoms.ChoiceAtom; import at.ac.tuwien.kr.alpha.core.programs.atoms.RuleAtom; import at.ac.tuwien.kr.alpha.core.programs.rules.InternalRule; +import org.apache.commons.lang3.tuple.ImmutablePair; +import org.apache.commons.lang3.tuple.Pair; +import org.apache.commons.lang3.tuple.Triple; + +import java.util.Arrays; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.SortedSet; +import java.util.TreeSet; +import java.util.stream.Stream; + +import static at.ac.tuwien.kr.alpha.commons.util.Util.entriesToMap; +import static at.ac.tuwien.kr.alpha.commons.util.Util.entry; +import static at.ac.tuwien.kr.alpha.core.common.NoGood.headFirst; +import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals; +import static java.util.Arrays.asList; +import static java.util.Collections.emptyList; /** * Represents a small ASP program with choices {@code { aa :- not bb. bb :- not aa. }}. @@ -185,6 +187,15 @@ public Pair, Map> getChoiceAtoms() { } } + @Override + public boolean inputProgramContainsWeakConstraints() { + return false; + } + + @Override + public List> getWeakConstraintInformation() { + return emptyList(); + } @Override public Map> getHeadsToBodies() { return Collections.emptyMap(); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java index fe2cb6f8c..d655b9aff 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/grounder/DummyGrounder.java @@ -33,11 +33,14 @@ import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals; import static java.util.Collections.singleton; import static java.util.Collections.singletonList; +import org.apache.commons.lang3.tuple.Triple; import java.util.Arrays; import java.util.Collections; +import static java.util.Collections.emptyList; import java.util.HashMap; import java.util.HashSet; +import java.util.List; import java.util.Map; import java.util.Set; import java.util.SortedSet; @@ -172,7 +175,17 @@ public Map getNoGoods(Assignment assignment) { public Pair, Map> getChoiceAtoms() { return new ImmutablePair<>(new HashMap<>(), new HashMap<>()); } - + + @Override + public boolean inputProgramContainsWeakConstraints() { + return false; + } + + @Override + public List> getWeakConstraintInformation() { + return emptyList(); + } + @Override public Map> getHeadsToBodies() { return Collections.emptyMap(); diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java index c0bfdd991..1d59e1dcd 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/SolverTests.java @@ -27,21 +27,6 @@ */ package at.ac.tuwien.kr.alpha.core.solver; -import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSet; -import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSets; -import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSetsWithBase; -import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.buildSolverForRegressionTest; -import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.collectRegressionTestAnswerSets; -import static java.util.Collections.singleton; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; - -import java.util.Collections; -import java.util.HashSet; -import java.util.List; -import java.util.Set; -import java.util.SortedSet; - import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.Solver; import at.ac.tuwien.kr.alpha.api.programs.ASPCore2Program; @@ -59,6 +44,21 @@ import at.ac.tuwien.kr.alpha.core.grounder.DummyGrounder; import at.ac.tuwien.kr.alpha.core.test.util.AnswerSetsParser; +import java.util.Collections; +import java.util.HashSet; +import java.util.List; +import java.util.Set; +import java.util.SortedSet; + +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSet; +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSets; +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertRegressionTestAnswerSetsWithBase; +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.buildSolverForRegressionTest; +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.collectRegressionTestAnswerSets; +import static java.util.Collections.singleton; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + public class SolverTests { private static class Thingy implements Comparable { @@ -82,7 +82,8 @@ public void testObjectProgram(RegressionTestConfig cfg) { final ASPCore2Program program = Programs.newASPCore2Program( Collections.emptyList(), Collections.singletonList(fact), - Programs.newInlineDirectives() + Programs.newInlineDirectives(), + false ); assertEquals(singleton(new AnswerSetBuilder() diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/WeakConstraintsTests.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/WeakConstraintsTests.java new file mode 100644 index 000000000..5c250f0cf --- /dev/null +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/WeakConstraintsTests.java @@ -0,0 +1,120 @@ +package at.ac.tuwien.kr.alpha.core.solver; + +import at.ac.tuwien.kr.alpha.api.AnswerSet; +import at.ac.tuwien.kr.alpha.core.test.util.TestUtils; + +import java.util.Set; + +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.assertOptimumAnswerSetEquals; +import static at.ac.tuwien.kr.alpha.core.test.util.TestUtils.collectRegressionTestOptimalAnswerSets; +import static org.junit.jupiter.api.Assertions.assertThrows; + +/** + * Copyright (c) 2021, the Alpha Team. + */ +public class WeakConstraintsTests { + + @RegressionTest + public void simpleWeightsSameLevel(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = ":~a.[1@0,foo,bar]" + + ":~b.[2@0,baz]" + + "a :- not b. b:- not a."; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals("a", "1@0", actualAnswerSets); + } + + + @RegressionTest + public void simpleWeightedAnswerSet(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = ":~a.[2@2,foo,bar]" + + ":~b.[1@1,baz]" + + "a :- not b. b:- not a."; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals("b", "1@1", actualAnswerSets); + } + + @RegressionTest + public void simpleWeightedAnswerSetWithNegativeLevel(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = ":~a.[2@1,foo,bar]" + + ":~b.[1@-1,baz]" + + "a :- not b. b:- not a."; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals("b", "1@-1", actualAnswerSets); + } + + @RegressionTest + public void simpleMultiLevelWeightedAnswerSet(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = ":~a.[2@2,foo,bar]" + + ":~b.[1@1,baz]" + + ":~b.[3@-4,baz]" + + "a :- not b. b:- not a."; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals("b", "3@-4, 1@1", actualAnswerSets); + } + + @RegressionTest + public void sameWeightSummedUpInLevel(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = "{a;b}." + + ":- not a, not b." + + ":~b.[1@3]" + + ":~a.[2@1,foo]" + + ":~a.[2@1,bar]"; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals("a", "4@1", actualAnswerSets); + } + + @RegressionTest + public void sameWeightSameTermNotSummedUpInLevel(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = "{a;b}." + + ":- not a, not b." + + "c :- a." + + ":~b.[1@3]" + + ":~a.[2@1,foo]" + + ":~c.[2@1,foo]"; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals("a, c", "2@1", actualAnswerSets); + } + + @RegressionTest + public void negativeWeightThrowsException(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = "p(1..9)." + + "a :- q(X)." + + "{ q(X) } :- p(X), X != 8. % exclude case where violation is 0, which could be encountered before negative weight.\n" + + "has_q :- q(X)." + + ":- not has_q." + + ":- q(X), q(Y), X != Y." + + "w(Z) :- Z = 8 - K, q(K)." + + ":~a,w(Z).[Z@1]"; + assertThrows(IllegalArgumentException.class, () -> { + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + // In case negative weights can be dealt with (e.g. by fully grounding or under certain restrictions), + // the optimum answer set of above program is: p(1),...,p(9),q(9),w(-1),a,has_q at valuation -1@1 + // Under current behaviour we expect the computation of answer-sets to fail already. + assertOptimumAnswerSetEquals( + "p(1),p(2),p(3),p(4),p(5),p(6),p(7),p(8),p(9),q(9),w(-1),a,has_q", "-1@1", actualAnswerSets); + }); + } + + @RegressionTest + public void complexValuationWithMultipleWeightsOnMultipleLevels(RegressionTestConfig cfg) { + TestUtils.ignoreTestForNaiveSolver(cfg); + String program = "dom(1..3)." + + "{ a(X) } :- dom(X)." + + "{ b(X) } :- dom(X)." + + "{ c(X) } :- dom(X)." + + "weightatlevel(W,L) :- a(X),b(Y),c(Z), W = 2*X+Y, L = Z*Y." + + ":~ weightatlevel(W,L).[W@L]" + + "has_wal :- weightatlevel(W,L)." + + ":- not has_wal."; + Set actualAnswerSets = collectRegressionTestOptimalAnswerSets(program, cfg); + assertOptimumAnswerSetEquals( + "dom(1), dom(2), dom(3), c(1), b(1), a(1), weightatlevel(3,1), has_wal", "3@1", actualAnswerSets); + } +} diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeightAtLevelsManagerTest.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeightAtLevelsManagerTest.java new file mode 100644 index 000000000..f9b63e598 --- /dev/null +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/solver/optimization/WeightAtLevelsManagerTest.java @@ -0,0 +1,150 @@ +package at.ac.tuwien.kr.alpha.core.solver.optimization; + +import org.junit.jupiter.api.Test; + +import java.util.TreeMap; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertFalse; +import static org.junit.jupiter.api.Assertions.assertNull; +import static org.junit.jupiter.api.Assertions.assertThrows; +import static org.junit.jupiter.api.Assertions.assertTrue; + +/** + * Copyright (c) 2021, the Alpha Team. + */ +public class WeightAtLevelsManagerTest { + + @Test + public void simpleWeightAtTwoLevels() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager(); + weightAtLevelsManager.setChecksEnabled(true); + weightAtLevelsManager.setMaxLevel(3); + assertTrue(weightAtLevelsManager.getCurrentWeightAtLevels().isEmpty()); + weightAtLevelsManager.increaseCurrentWeight(0, 2); + weightAtLevelsManager.increaseCurrentWeight(3, 1); + TreeMap currentWeightsAfterIncrease = weightAtLevelsManager.getCurrentWeightAtLevels(); + assertEquals(1, currentWeightsAfterIncrease.get(3).longValue()); + assertEquals(2, currentWeightsAfterIncrease.get(0).longValue()); + assertEquals(2, currentWeightsAfterIncrease.size()); + + weightAtLevelsManager.decreaseCurrentWeight(0, 2); + + TreeMap currentWeightsAfterDecrease = weightAtLevelsManager.getCurrentWeightAtLevels(); + assertEquals(1, currentWeightsAfterDecrease.get(3).longValue()); + assertNull(currentWeightsAfterDecrease.get(0)); + assertEquals(1, currentWeightsAfterDecrease.size()); + } + + @Test + public void currentIsBestAfterDecrease() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager(); + weightAtLevelsManager.setChecksEnabled(true); + weightAtLevelsManager.setMaxLevel(0); + assertTrue(weightAtLevelsManager.getCurrentWeightAtLevels().isEmpty()); + weightAtLevelsManager.increaseCurrentWeight(0, 2); + weightAtLevelsManager.increaseCurrentWeight(0, 2); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + + assertFalse(weightAtLevelsManager.isCurrentBetterThanBest()); + + weightAtLevelsManager.decreaseCurrentWeight(0, 2); + assertTrue(weightAtLevelsManager.isCurrentBetterThanBest()); + } + + @Test + public void addAtomOnHigherThanMaxLevel() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager(); + weightAtLevelsManager.setChecksEnabled(true); + weightAtLevelsManager.setMaxLevel(3); + assertTrue(weightAtLevelsManager.getCurrentWeightAtLevels().isEmpty()); + weightAtLevelsManager.increaseCurrentWeight(3, 1); + weightAtLevelsManager.increaseCurrentWeight(0, 2); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + + assertFalse(weightAtLevelsManager.isCurrentBetterThanBest()); + + weightAtLevelsManager.decreaseCurrentWeight(0, 2); + assertTrue(weightAtLevelsManager.isCurrentBetterThanBest()); + // Now increase some weight at a level beyond the declared maxLevel, so an Exception is expected here. + assertThrows(RuntimeException.class, () -> { + weightAtLevelsManager.increaseCurrentWeight(4, 3); + }); + } + + @Test + public void markingCurrentWeightAsBestDecreasesMaximumLevel() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager(); + weightAtLevelsManager.setChecksEnabled(true); + weightAtLevelsManager.setMaxLevel(3); + assertTrue(weightAtLevelsManager.getCurrentWeightAtLevels().isEmpty()); + weightAtLevelsManager.increaseCurrentWeight(1, 1); + + assertEquals(3, weightAtLevelsManager.getMaxLevel()); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + assertTrue(weightAtLevelsManager.getMaxLevel() < 3); + } + + @Test + public void indirectTrimmingCheck() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager(); + weightAtLevelsManager.setChecksEnabled(true); + weightAtLevelsManager.setMaxLevel(4); + assertTrue(weightAtLevelsManager.getCurrentWeightAtLevels().isEmpty()); + weightAtLevelsManager.increaseCurrentWeight(4, 1); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + + weightAtLevelsManager.decreaseCurrentWeight(4, 1); + weightAtLevelsManager.increaseCurrentWeight(2, 1); + weightAtLevelsManager.increaseCurrentWeight(1, 3); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + weightAtLevelsManager.decreaseCurrentWeight(1, 3); + // Note: the below assertion relies on the implementation of WeightAtLevelsManager doing trimming. + assertTrue(weightAtLevelsManager.getMaxLevel() < 3); + } + + @Test + public void trimmingAtLevelZero() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager(); + weightAtLevelsManager.setChecksEnabled(true); + weightAtLevelsManager.setMaxLevel(3); + assertTrue(weightAtLevelsManager.getCurrentWeightAtLevels().isEmpty()); + weightAtLevelsManager.increaseCurrentWeight(2, 1); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + + weightAtLevelsManager.decreaseCurrentWeight(2, 1); + weightAtLevelsManager.increaseCurrentWeight(1, 1); + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + weightAtLevelsManager.decreaseCurrentWeight(1, 1); + + weightAtLevelsManager.markCurrentWeightAsBestKnown(); + assertFalse(weightAtLevelsManager.isCurrentBetterThanBest()); + } + + @Test + public void initializationWithMaxBound() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager("1@1,5@6,3@2"); + weightAtLevelsManager.setChecksEnabled(true); + assertTrue(weightAtLevelsManager.isCurrentBetterThanBest()); + } + + @Test + public void initializationWithMaxBoundAllowsBetterUntilBound() { + WeightAtLevelsManager weightAtLevelsManager = new WeightAtLevelsManager("1@2,4@3"); + weightAtLevelsManager.setChecksEnabled(true); + TreeMap initialWeights = weightAtLevelsManager.getCurrentWeightAtLevels(); + assertEquals(initialWeights.size(), 0); + assertTrue(weightAtLevelsManager.isCurrentBetterThanBest()); + weightAtLevelsManager.increaseCurrentWeight(2, 1); + assertTrue(weightAtLevelsManager.isCurrentBetterThanBest()); + weightAtLevelsManager.increaseCurrentWeight(3, 3); + assertTrue(weightAtLevelsManager.isCurrentBetterThanBest()); + weightAtLevelsManager.increaseCurrentWeight(3, 1); + assertFalse(weightAtLevelsManager.isCurrentBetterThanBest()); + } + + @Test + public void initializationWithEmptyMaxBoundThrowsException() { + assertThrows(IllegalArgumentException.class, () -> new WeightAtLevelsManager("")); + } +} \ No newline at end of file diff --git a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java index bd0c358c1..4d29ae2ba 100644 --- a/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java +++ b/alpha-core/src/test/java/at/ac/tuwien/kr/alpha/core/test/util/TestUtils.java @@ -31,6 +31,7 @@ import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom; import at.ac.tuwien.kr.alpha.api.programs.terms.Term; import at.ac.tuwien.kr.alpha.commons.Predicates; +import at.ac.tuwien.kr.alpha.commons.WeightedAnswerSet; import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms; import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms; import at.ac.tuwien.kr.alpha.core.common.AtomStore; @@ -54,7 +55,7 @@ public static void fillAtomStore(AtomStore atomStore, int numberOfAtomsToFill) { atomStore.putIfAbsent(Atoms.newBasicAtom(predA, Terms.newConstant(i))); } } - + public static Atom atom(String predicateName, String... termStrings) { Term[] terms = new Term[termStrings.length]; for (int i = 0; i < termStrings.length; i++) { @@ -75,11 +76,11 @@ public static Atom atom(String predicateName, int... termInts) { } return Atoms.newBasicAtom(Predicates.getPredicate(predicateName, terms.length), terms); } - + public static void printNoGoods(AtomStore atomStore, Collection noGoods) { System.out.println(noGoods.stream().map(atomStore::noGoodToString).collect(Collectors.toSet())); } - + public static void assertAnswerSetsEqual(Set expected, Set actual) { if (expected == null) { if (actual != null) { @@ -161,15 +162,24 @@ private static Solver buildSolverFromSystemConfig(ASPCore2Program prog, SystemCo : InternalProgram.fromNormalProgram(normalProg); return SolverFactory.getInstance(cfg, atomStore, GrounderFactory.getInstance(cfg.getGrounderName(), preprocessed, atomStore, cfg.isDebugInternalChecks())); } - + public static Solver buildSolverForRegressionTest(ASPCore2Program prog, RegressionTestConfig cfg) { return buildSolverFromSystemConfig(prog, cfg.toSystemConfig()); } - + + public static Solver buildSolverForOptimizationRegressionTest(ASPCore2Program prog, RegressionTestConfig cfg) { + SystemConfig systemConfig = cfg.toSystemConfig(); + systemConfig.setAnswerSetOptimizationEnabled(true); + return buildSolverFromSystemConfig(prog, systemConfig); + } + + public static Set collectRegressionTestOptimalAnswerSets(String prog, RegressionTestConfig config) { + return buildSolverForOptimizationRegressionTest(new ProgramParserImpl().parse(prog), config).collectSet(); + } public static Solver buildSolverForRegressionTest(String prog, RegressionTestConfig cfg) { return buildSolverFromSystemConfig(new ProgramParserImpl().parse(prog), cfg.toSystemConfig()); } - + public static Solver buildSolverForRegressionTest(AtomStore atomStore, Grounder grounder, RegressionTestConfig cfg) { SystemConfig systemCfg = cfg.toSystemConfig(); return SolverFactory.getInstance(systemCfg, atomStore, grounder); @@ -178,7 +188,7 @@ public static Solver buildSolverForRegressionTest(AtomStore atomStore, Grounder public static Set collectRegressionTestAnswerSets(ASPCore2Program prog, RegressionTestConfig cfg) { return buildSolverForRegressionTest(prog, cfg).collectSet(); } - + public static Set collectRegressionTestAnswerSets(String aspstr, RegressionTestConfig cfg) { ASPCore2Program prog = new ProgramParserImpl().parse(aspstr); return collectRegressionTestAnswerSets(prog, cfg); @@ -188,32 +198,62 @@ public static void assertRegressionTestAnswerSet(RegressionTestConfig cfg, Strin Set actualAnswerSets = collectRegressionTestAnswerSets(program, cfg); TestUtils.assertAnswerSetsEqual(answerSet, actualAnswerSets); } - + public static void assertRegressionTestAnswerSets(RegressionTestConfig cfg, String program, String... answerSets) { Set actualAnswerSets = collectRegressionTestAnswerSets(program, cfg); - TestUtils.assertAnswerSetsEqual(answerSets, actualAnswerSets); + TestUtils.assertAnswerSetsEqual(answerSets, actualAnswerSets); } - + public static void assertRegressionTestAnswerSetsWithBase(RegressionTestConfig cfg, String program, String base, String... answerSets) { Set actualAnswerSets = collectRegressionTestAnswerSets(program, cfg); - TestUtils.assertAnswerSetsEqualWithBase(base, answerSets, actualAnswerSets); + TestUtils.assertAnswerSetsEqualWithBase(base, answerSets, actualAnswerSets); } - + public static void runWithTimeout(RegressionTestConfig cfg, long baseTimeout, long timeoutFactor, Executable action) { long timeout = cfg.isDebugChecks() ? timeoutFactor * baseTimeout : baseTimeout; assertTimeoutPreemptively(Duration.ofMillis(timeout), action); } - + public static void ignoreTestForNaiveSolver(RegressionTestConfig cfg) { Assumptions.assumeFalse(cfg.getSolverName().equals("naive")); } - + public static void ignoreTestForNonDefaultDomainIndependentHeuristics(RegressionTestConfig cfg) { Assumptions.assumeTrue(cfg.getBranchingHeuristic() == Heuristic.VSIDS); } - + public static void ignoreTestForSimplifiedSumAggregates(RegressionTestConfig cfg) { Assumptions.assumeTrue(cfg.isSupportNegativeSumElements()); } + public static WeightedAnswerSet weightedAnswerSetFromStrings(String basicAnswerSetAsString, String weightAtLevelsAsString) { + AnswerSet basicAnswerSet = AnswerSetsParser.parse("{ " + basicAnswerSetAsString + " }").iterator().next(); + return new WeightedAnswerSet(basicAnswerSet, WeightedAnswerSet.weightPerLevelFromString(weightAtLevelsAsString)); + } + + public static void assertOptimumAnswerSetEquals(String expectedOptimumAnswerSet, String expectedWeightsAtLevels, Set actual) { + WeightedAnswerSet optimumAnswerSet = weightedAnswerSetFromStrings(expectedOptimumAnswerSet, expectedWeightsAtLevels); + // Check the optimum is contained in the set of actual answer sets. + if (!actual.contains(optimumAnswerSet)) { + throw new AssertionError("Expected optimum answer set is not contained in actual.\n" + + "Expected optimum answer set: " + optimumAnswerSet + "\n" + + "Actual answer sets: " + actual); + } + // Ensure that there is no better answer set contained in the actual answer sets. + for (AnswerSet actualAnswerSet : actual) { + if (actualAnswerSet.equals(optimumAnswerSet)) { + // Skip optimum itself. + continue; + } + if (!(actualAnswerSet instanceof WeightedAnswerSet)) { + throw new AssertionError("Expecting weighted answer sets but obtained answer set is not: " + actualAnswerSet); + } + WeightedAnswerSet actualWeightedAnswerSet = (WeightedAnswerSet) actualAnswerSet; + if (optimumAnswerSet.compareWeights(actualWeightedAnswerSet) >= 0) { + throw new AssertionError("Actual answer set is better than expected one.\n" + + "Expected: " + optimumAnswerSet + "\n" + + "Actual: " + actualWeightedAnswerSet); + } + } + } } diff --git a/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java b/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java index e359284a1..58a7bb68f 100644 --- a/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java +++ b/alpha-solver/src/main/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImpl.java @@ -27,25 +27,6 @@ */ package at.ac.tuwien.kr.alpha.api.impl; -import java.io.IOException; -import java.io.InputStream; -import java.nio.channels.Channels; -import java.nio.file.Files; -import java.nio.file.Path; -import java.nio.file.Paths; -import java.util.Collections; -import java.util.List; -import java.util.Map; -import java.util.Set; -import java.util.stream.Collectors; -import java.util.stream.Stream; - -import org.apache.commons.lang3.StringUtils; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import com.google.common.annotations.VisibleForTesting; - import at.ac.tuwien.kr.alpha.api.Alpha; import at.ac.tuwien.kr.alpha.api.AnswerSet; import at.ac.tuwien.kr.alpha.api.DebugSolvingContext; @@ -79,6 +60,23 @@ import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation; import at.ac.tuwien.kr.alpha.core.programs.transformation.StratifiedEvaluation; import at.ac.tuwien.kr.alpha.core.solver.SolverFactory; +import com.google.common.annotations.VisibleForTesting; +import org.apache.commons.lang3.StringUtils; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.io.IOException; +import java.io.InputStream; +import java.nio.channels.Channels; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Collections; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; +import java.util.stream.Stream; public class AlphaImpl implements Alpha { @@ -157,7 +155,7 @@ InternalProgram performProgramPreprocessing(NormalProgram program) { LOGGER.debug("Preprocessing InternalProgram!"); InternalProgram retVal = InternalProgram.fromNormalProgram(program); if (config.isEvaluateStratifiedPart()) { - AnalyzedProgram analyzed = new AnalyzedProgram(retVal.getRules(), retVal.getFacts()); + AnalyzedProgram analyzed = new AnalyzedProgram(retVal.getRules(), retVal.getFacts(), program.containsWeakConstraints()); retVal = new StratifiedEvaluation().apply(analyzed); } return retVal; diff --git a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java index 7bda46edc..4a9b7cc68 100644 --- a/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java +++ b/alpha-solver/src/test/java/at/ac/tuwien/kr/alpha/api/impl/AlphaImplTest.java @@ -326,7 +326,7 @@ public void withExternalSubtype() throws Exception { Alpha system = new AlphaImpl(); - ASPCore2Program prog = Programs.newASPCore2Program(singletonList(rule), emptyList(), Programs.newInlineDirectives()); + ASPCore2Program prog = Programs.newASPCore2Program(singletonList(rule), emptyList(), Programs.newInlineDirectives(), false); Set actual = system.solve(prog).collect(Collectors.toSet()); Set expected = new HashSet<>(singletonList(new AnswerSetBuilder().predicate("p").instance("x").build())); diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar index 7454180f2..943f0cbfa 100644 Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index f42e62f37..2b22d057a 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,6 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists distributionUrl=https\://services.gradle.org/distributions/gradle-7.6-all.zip +networkTimeout=10000 zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/gradlew b/gradlew index c53aefaa5..65dcd68d6 100755 --- a/gradlew +++ b/gradlew @@ -1,7 +1,7 @@ #!/bin/sh # -# Copyright © 2015-2021 the original authors. +# Copyright © 2015-2021 the original authors. # # Licensed under the Apache License, Version 2.0 (the "License"); # you may not use this file except in compliance with the License. @@ -32,10 +32,10 @@ # Busybox and similar reduced shells will NOT work, because this script # requires all of these POSIX shell features: # * functions; -# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», -# «${var#prefix}», «${var%suffix}», and «$( cmd )»; -# * compound commands having a testable exit status, especially «case»; -# * various built-in commands including «command», «set», and «ulimit». +# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», +# «${var#prefix}», «${var%suffix}», and «$( cmd )»; +# * compound commands having a testable exit status, especially «case»; +# * various built-in commands including «command», «set», and «ulimit». # # Important for patching: # @@ -55,7 +55,7 @@ # Darwin, MinGW, and NonStop. # # (3) This script is generated from the Groovy template -# https://github.com/gradle/gradle/blob/master/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt +# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt # within the Gradle project. # # You can find Gradle at https://github.com/gradle/gradle/. @@ -80,10 +80,10 @@ do esac done -APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit - -APP_NAME="Gradle" +# This is normally unused +# shellcheck disable=SC2034 APP_BASE_NAME=${0##*/} +APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit # Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' @@ -143,12 +143,16 @@ fi if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then case $MAX_FD in #( max*) + # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 MAX_FD=$( ulimit -H -n ) || warn "Could not query maximum file descriptor limit" esac case $MAX_FD in #( '' | soft) :;; #( *) + # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 ulimit -n "$MAX_FD" || warn "Could not set maximum file descriptor limit to $MAX_FD" esac @@ -205,6 +209,12 @@ set -- \ org.gradle.wrapper.GradleWrapperMain \ "$@" +# Stop when "xargs" is not available. +if ! command -v xargs >/dev/null 2>&1 +then + die "xargs is not available" +fi + # Use "xargs" to parse quoted args. # # With -n1 it outputs one arg per line, with the quotes and backslashes removed. diff --git a/gradlew.bat b/gradlew.bat index ac1b06f93..6689b85be 100644 --- a/gradlew.bat +++ b/gradlew.bat @@ -14,7 +14,7 @@ @rem limitations under the License. @rem -@if "%DEBUG%" == "" @echo off +@if "%DEBUG%"=="" @echo off @rem ########################################################################## @rem @rem Gradle startup script for Windows @@ -25,7 +25,8 @@ if "%OS%"=="Windows_NT" setlocal set DIRNAME=%~dp0 -if "%DIRNAME%" == "" set DIRNAME=. +if "%DIRNAME%"=="" set DIRNAME=. +@rem This is normally unused set APP_BASE_NAME=%~n0 set APP_HOME=%DIRNAME% @@ -40,7 +41,7 @@ if defined JAVA_HOME goto findJavaFromJavaHome set JAVA_EXE=java.exe %JAVA_EXE% -version >NUL 2>&1 -if "%ERRORLEVEL%" == "0" goto execute +if %ERRORLEVEL% equ 0 goto execute echo. echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. @@ -75,13 +76,15 @@ set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar :end @rem End local scope for the variables with windows NT shell -if "%ERRORLEVEL%"=="0" goto mainEnd +if %ERRORLEVEL% equ 0 goto mainEnd :fail rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of rem the _cmd.exe /c_ return code! -if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1 -exit /b 1 +set EXIT_CODE=%ERRORLEVEL% +if %EXIT_CODE% equ 0 set EXIT_CODE=1 +if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE% +exit /b %EXIT_CODE% :mainEnd if "%OS%"=="Windows_NT" endlocal