Enable weak constraints

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<AnswerSet> {
 	 */
 	SortedSet<Atom> getPredicateInstances(Predicate predicate);
 
+	/**
+	 * Returns a mapping of {@link Predicate}s to all respective instances.
+	 */
+	Map<Predicate, SortedSet<Atom>> getPredicateInstances();
+
 	/**
 	 * Boolean flag indicating whether this {@link AnswerSet} represents the empty set.
 	 */

alpha-api/src/main/java/at/ac/tuwien/kr/alpha/api/Solver.java

@@ -38,4 +38,12 @@ default List<AnswerSet> 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();
+
 }

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;
+	}
 }

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<R extends Rule<? extends Head>> {
 	 */
 	List<R> getRules();
 
+	/**
+	 * Indicates whether this program contains some weak constraints.
+	 * @return true iff this program contains weak constraints.
+	 */
+	boolean containsWeakConstraints();
+
 }

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<String> fmt = new SimpleAnswerSetFormatter(sysCfg.getAtomSeparator());
 			BiConsumer<Integer, AnswerSet> 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<Integer, AnswerSet> 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

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));
+	}
 }

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<Predicate> predicates;
@@ -45,6 +46,11 @@ public boolean isEmpty() {
 		return predicates.isEmpty();
 	}
 
+	@Override
+	public Map<Predicate, SortedSet<Atom>> 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<Predicate> predicates = this.getPredicates();
 		int result = Util.compareSortedSets(predicates, other.getPredicates());