Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add additional simple support nogoods #226

Closed
wants to merge 6 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
87 changes: 52 additions & 35 deletions src/main/java/at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/**
* Copyright (c) 2016-2019, the Alpha Team.
/*
* Copyright (c) 2016-2020, the Alpha Team.
* All rights reserved.
*
* Additional changes made by Siemens.
Expand Down Expand Up @@ -130,7 +130,7 @@ private NaiveGrounder(InternalProgram program, AtomStore atomStore, GrounderHeur
final Set<InternalRule> uniqueGroundRulePerGroundHead = getRulesWithUniqueHead();
choiceRecorder = new ChoiceRecorder(atomStore);
noGoodGenerator = new NoGoodGenerator(atomStore, choiceRecorder, factsFromProgram, this.program, uniqueGroundRulePerGroundHead);

this.debugInternalChecks = debugInternalChecks;

// Initialize RuleInstantiator and instantiation strategy. Note that the instantiation strategy also
Expand Down Expand Up @@ -181,34 +181,51 @@ private Set<InternalRule> getRulesWithUniqueHead() {
final Set<InternalRule> uniqueGroundRulePerGroundHead = new HashSet<>();

for (Map.Entry<Predicate, LinkedHashSet<InternalRule>> headDefiningRules : program.getPredicateDefiningRules().entrySet()) {
if (headDefiningRules.getValue().size() != 1) {
final LinkedHashSet<InternalRule> rules = headDefiningRules.getValue();
if (rules.size() != 1 && !areAllRulesGround(rules)) {
continue;
}

InternalRule nonGroundRule = headDefiningRules.getValue().iterator().next();
// Check that all variables of the body also occur in the head (otherwise grounding is not unique).
Atom headAtom = nonGroundRule.getHeadAtom();

// Rule is not guaranteed unique if there are facts for it.
HashSet<Instance> potentialFacts = factsFromProgram.get(headAtom.getPredicate());
if (potentialFacts != null && !potentialFacts.isEmpty()) {
continue;
for (InternalRule internalRule : rules) {
if (isRuleUniquePerGroundHead(internalRule)) {
uniqueGroundRulePerGroundHead.add(internalRule);
}
}
}
return uniqueGroundRulePerGroundHead;
}

// Collect head and body variables.
HashSet<VariableTerm> occurringVariablesHead = new HashSet<>(headAtom.toLiteral().getBindingVariables());
HashSet<VariableTerm> occurringVariablesBody = new HashSet<>();
for (Literal lit : nonGroundRule.getPositiveBody()) {
occurringVariablesBody.addAll(lit.getBindingVariables());
}
occurringVariablesBody.removeAll(occurringVariablesHead);
private boolean isRuleUniquePerGroundHead(InternalRule internalRule) {
// Check that all variables of the body also occur in the head (otherwise grounding is not unique).
Atom headAtom = internalRule.getHeadAtom();

// Rule is not guaranteed unique if there are facts for it.
HashSet<Instance> potentialFacts = factsFromProgram.get(headAtom.getPredicate());
if (potentialFacts != null && !potentialFacts.isEmpty()) {
return false;
}

// Check if ever body variables occurs in the head.
if (occurringVariablesBody.isEmpty()) {
uniqueGroundRulePerGroundHead.add(nonGroundRule);
// Collect head and body variables.
HashSet<VariableTerm> occurringVariablesHead = new HashSet<>(headAtom.toLiteral().getBindingVariables());
HashSet<VariableTerm> occurringVariablesBody = new HashSet<>();
for (Literal lit : internalRule.getPositiveBody()) {
occurringVariablesBody.addAll(lit.getBindingVariables());
}
occurringVariablesBody.removeAll(occurringVariablesHead);

// Check if ever body variables occurs in the head.
return occurringVariablesBody.isEmpty();
}

private boolean areAllRulesGround(Collection<InternalRule> rules) {
boolean allGround = true;
for (InternalRule internalRule : rules) {
if (!internalRule.isGround()) {
allGround = false;
break;
}
}
return uniqueGroundRulePerGroundHead;
return allGround;
}

/**
Expand Down Expand Up @@ -276,10 +293,10 @@ public AnswerSet assignmentToAnswerSet(Iterable<Integer> trueAtoms) {
if (knownPredicates.isEmpty()) {
return BasicAnswerSet.EMPTY;
}

return new BasicAnswerSet(knownPredicates, predicateInstances);
}

/**
* Prepares facts of the input program for joining and derives all NoGoods representing ground rules. May only be called once.
* @return
Expand Down Expand Up @@ -427,12 +444,12 @@ BindingResult getGroundInstantiations(InternalRule rule, RuleGroundingOrder grou

/**
* Helper method used by {@link NaiveGrounder#bindNextAtomInRule(RuleGroundingOrder, int, int, int, Substitution)}.
*
*
* Takes an <code>ImmutablePair</code> of a {@link Substitution} and an accompanying {@link AssignmentStatus} and calls
* <code>bindNextAtomInRule</code> for the next literal in the grounding order.
* If the assignment status for the last bound literal was {@link AssignmentStatus#UNASSIGNED}, the <code>remainingTolerance</code>
* parameter is decreased by 1. If the remaining tolerance drops below zero, this method returns an empty {@link BindingResult}.
*
*
* @param groundingOrder
* @param orderPosition
* @param originalTolerance
Expand All @@ -449,8 +466,8 @@ private BindingResult continueBinding(RuleGroundingOrder groundingOrder, int ord
case TRUE:
return advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, remainingTolerance, substitution);
case UNASSIGNED:
// The last literal bound to obtain the current substitution has not been assigned a truth value by the solver yet.
// If we still have enough tolerance, we can continue grounding nevertheless.
// The last literal bound to obtain the current substitution has not been assigned a truth value by the solver yet.
// If we still have enough tolerance, we can continue grounding nevertheless.
int toleranceForNextRun = remainingTolerance - 1;
if (toleranceForNextRun >= 0) {
return advanceAndBindNextAtomInRule(groundingOrder, orderPosition, originalTolerance, toleranceForNextRun, substitution);
Expand Down Expand Up @@ -483,11 +500,11 @@ private BindingResult pushBackAndBindNextAtomInRule(RuleGroundingOrder grounding
//@formatter:off
/**
* Computes ground substitutions for a literal based on a {@link RuleGroundingOrder} and a {@link Substitution}.
*
*
* Computes ground substitutions for the literal at position <code>orderPosition</code> of <code>groundingOrder</code>
* Actual substitutions are computed by this grounder's {@link LiteralInstantiator}.
*
* @param groundingOrder a {@link RuleGroundingOrder} representing the body literals of a rule in the
* Actual substitutions are computed by this grounder's {@link LiteralInstantiator}.
*
* @param groundingOrder a {@link RuleGroundingOrder} representing the body literals of a rule in the
* sequence in which the should be bound during grounding.
* @param orderPosition the current position within <code>groundingOrder</code>, indicates which literal should be bound
* @param originalTolerance the original tolerance of the used grounding heuristic
Expand Down Expand Up @@ -536,7 +553,7 @@ private BindingResult bindNextAtomInRule(RuleGroundingOrder groundingOrder, int
*/
if (originalTolerance > 0) {
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,
// 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);
} else {
Expand Down Expand Up @@ -607,7 +624,7 @@ public Set<Literal> justifyAtom(int atomToJustify, Assignment currentAssignment)
/**
* Checks that every nogood not marked as {@link NoGoodInterface.Type#INTERNAL} contains only
* atoms which are not {@link Predicate#isSolverInternal()} (except {@link RuleAtom}s, which are allowed).
*
*
* @param newNoGoods
*/
private void checkTypesOfNoGoods(Collection<NoGood> newNoGoods) {
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
/**
* Copyright (c) 2017-2018, the Alpha Team.
/*
* Copyright (c) 2017-2020, the Alpha Team.
* All rights reserved.
*
* Additional changes made by Siemens.
Expand Down Expand Up @@ -72,7 +72,7 @@ public class NoGoodGenerator {

/**
* Generates all NoGoods resulting from a non-ground rule and a variable substitution.
*
*
* @param nonGroundRule
* the non-ground rule.
* @param substitution
Expand All @@ -97,7 +97,7 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final InternalRule nonGroundR

final Atom groundHeadAtom = nonGroundRule.getHeadAtom().substitute(substitution);
final int headId = atomStore.putIfAbsent(groundHeadAtom);

// Prepare atom representing the rule body.
final RuleAtom bodyAtom = new RuleAtom(nonGroundRule, substitution);

Expand All @@ -113,7 +113,7 @@ List<NoGood> generateNoGoodsFromGroundSubstitution(final InternalRule nonGroundR
final int headLiteral = atomToLiteral(atomStore.putIfAbsent(nonGroundRule.getHeadAtom().substitute(substitution)));

choiceRecorder.addHeadToBody(headId, atomOf(bodyRepresentingLiteral));

// Create a nogood for the head.
result.add(NoGood.headFirst(negateLiteral(headLiteral), bodyRepresentingLiteral));

Expand Down