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

Conflict generalisation #242

Draft
wants to merge 60 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
60 commits
Select commit Hold shift + click to select a range
5e41ba8
Add references to original nogoods to Antecedents
rtaupe Mar 20, 2020
a5c6a9b
Introduce NonGroundNoGood
rtaupe Mar 20, 2020
0cf2dbc
Generate first non-ground nogood (for head of rule)
rtaupe Mar 20, 2020
16ca3fe
Generate non-ground nogoods for static rule nogoods
rtaupe Mar 23, 2020
2d8689d
Reset rule IDs before running tests
rtaupe Mar 23, 2020
ff97640
Satisfy Checkstyle
rtaupe Mar 23, 2020
46b9883
Generate non-ground nogoods for static constraint nogoods
rtaupe Mar 23, 2020
b545c27
Remember original nogoods in binary watch list
rtaupe Mar 23, 2020
95e5914
Learn non-ground nogoods (preliminary implementation)
rtaupe Mar 23, 2020
350e7ab
Include variables in non-ground rule atom
rtaupe Mar 24, 2020
674aa8f
Fix: do not try to find atom in conflict reason
rtaupe Mar 24, 2020
e628068
Do not add the same original nogood twice to binary watch list
rtaupe Mar 25, 2020
e84056f
Remove faulty code from conflict generalisation
rtaupe Mar 25, 2020
2f20021
Skeleton for separate conflict analysis method
rtaupe Mar 25, 2020
d7c1b25
Remove conflict generalisation code from #analyzeTrailBased
rtaupe Mar 25, 2020
21de49b
Merge branch 'master' into conflict_generalisation
rtaupe Mar 25, 2020
ecd6bd4
Extract ConflictAnalysisResult to separate file
rtaupe Mar 25, 2020
d19f95a
Re-implement CDNL without 1UIP
rtaupe Mar 25, 2020
5c628ea
Learn nogoods on all UIPs
rtaupe Mar 25, 2020
bc1957e
Use underlying ground learner in non-ground learner
rtaupe Mar 25, 2020
a37eceb
Fix re-implementation of 1UIP learning by using trail walker
rtaupe Mar 27, 2020
af1160e
If current DL = 0, learn nothing and return UNSAT
rtaupe Mar 27, 2020
0cb9bcc
1UIP learning: consider sophisticated techniques to prove UNSAT
rtaupe Mar 31, 2020
0cfa69c
Make variable names unique in nogoods before resolution
rtaupe Apr 1, 2020
e838da0
Move substitution stuff from grounder to common
rtaupe Apr 1, 2020
4de090c
Fix visibility of Substitution constructor and method
rtaupe Apr 1, 2020
5c24ad9
Implement explanation-based learning of non-ground constraints
rtaupe Apr 3, 2020
498a008
Substitution: left constant / right variable is unsupported
rtaupe Apr 7, 2020
19d1fec
Fix get...Variables in BodyRepresentingLiteral
rtaupe Apr 7, 2020
59b1f18
Logging: output learned non-ground nogoods
rtaupe Apr 7, 2020
7890cb7
Output learned non-ground nogoods with counters
rtaupe Apr 7, 2020
1c1dd68
GroundAndNonGroundNoGood#toString
rtaupe Apr 7, 2020
dc663bc
Fix unification of conflicting atoms during non-ground resolution
rtaupe Apr 7, 2020
ae2cfc3
Satisfy Checkstyle
rtaupe Apr 8, 2020
2c33c21
Apply conflict unifier to whole non-ground nogood
rtaupe Apr 8, 2020
b4cdc6b
Implement NonGroundNoGood#equals() and hashCode() and compareTo
rtaupe Apr 8, 2020
b27e283
Enable more kinds of unifiers
rtaupe Apr 9, 2020
edc03ca
stop conflict generalisation after 1000 conflicts
rtaupe Apr 17, 2020
1a5660f
Move SubsitutionTest to common package
rtaupe Apr 22, 2020
b3484a0
Move SubsitutionTest to common package
rtaupe Apr 22, 2020
87adc46
Merge branch 'move_substitution_test' into conflict_generalisation
rtaupe Apr 22, 2020
fafecf1
move method parseTerm from Substitution to ProgramPartParser
rtaupe Apr 22, 2020
80b0cf1
use ProgramPartParser to construct literals for unit tests
rtaupe Apr 22, 2020
06d8199
Merge branch 'program_part_parser' into conflict_generalisation
rtaupe Apr 22, 2020
d61a4a6
Fix: ProgramPartParser must accept variables
rtaupe Apr 23, 2020
7ae49ea
Merge branch 'program_part_parser' into conflict_generalisation
rtaupe Apr 23, 2020
9c47b90
Throw exception if variable name is invalid
rtaupe Apr 23, 2020
18c50ba
Merge branch 'forbid_lowercase_variable_terms' into conflict_generali…
rtaupe Apr 23, 2020
6934d80
Do not learn multiple equivalent non-ground nogoods
rtaupe Apr 23, 2020
a877134
Output most effective learned non-ground nogoods as constraints
rtaupe Apr 23, 2020
2e89d91
Simplify variable names in learned nogoods
rtaupe Apr 23, 2020
276b8d5
Further simplify variable names in learned nogoods
rtaupe Apr 23, 2020
fa045d0
Do not attempt to print violated nogoods if there are none
rtaupe May 3, 2020
ef7a796
Satisfy CheckStyle
rtaupe Jul 12, 2020
d84305a
Log all learned non-ground nogoods if ...
rtaupe Jul 13, 2020
5a5f6a2
Learn non-ground nogood from non-UIP
rtaupe Jul 15, 2020
cf8a47f
Output all learned constraints ordered by number of violations
rtaupe Jul 15, 2020
d56eea4
Fix bug in NonGroundNoGood#simplifyVariableNames
rtaupe Jul 22, 2020
f5e8824
use also literals assigned at DL below current DL for resolution
rtaupe Jul 22, 2020
aa79539
Satisfy CheckStyle
rtaupe Sep 8, 2020
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
Prev Previous commit
Next Next commit
1UIP learning: consider sophisticated techniques to prove UNSAT
  • Loading branch information
rtaupe committed Mar 31, 2020
commit 0cb9bcc3d14059fe654698cc2217320dcd185b7d
Original file line number Diff line number Diff line change
@@ -140,7 +140,18 @@ private ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason) {
return analyzeTrailBased(conflictReason, true);
}

ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason, boolean minimizeLearnedNoGood) {
/**
* Analyzes a conflict based on the trail assignment.
* @param conflictReason the violated nogood
* @param optimizeAnalysisResult if {@code true}, the analysis result will be optimized in two ways:
* <ol>
* <li>if the learned nogood is not assigning due to out-of-order assigned literals
* and thus the program can be proven to be UNSAT, UNSAT will be returned</li>
* <li>the learned nogood will be minimized by local clause minimization</li>
* </ol>
* @return an instance of {@link ConflictAnalysisResult} that may contain a learned nogood or the information that the problem is UNSAT.
*/
ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason, boolean optimizeAnalysisResult) {
LOGGER.trace("Analyzing trail based.");
if (assignment.getDecisionLevel() == 0) {
LOGGER.trace("Conflict on decision level 0.");
@@ -206,7 +217,7 @@ ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason, boolean mini
resolutionLiterals.add(atomToLiteral(nextAtom, assignment.getTruth(nextAtom).toBoolean()));

final int[] learnedLiterals;
if (minimizeLearnedNoGood) {
if (optimizeAnalysisResult) {
learnedLiterals = minimizeLearnedLiterals(resolutionLiterals, seenAtoms);
} else {
learnedLiterals = new int[resolutionLiterals.size()];
@@ -223,10 +234,14 @@ ConflictAnalysisResult analyzeTrailBased(Antecedent conflictReason, boolean mini

int backjumpingDecisionLevel = computeBackjumpingDecisionLevel(learnedNoGood);
if (backjumpingDecisionLevel < 0) {
// Due to out-of-order assigned literals, the learned nogood may be not assigning.
backjumpingDecisionLevel = computeConflictFreeBackjumpingLevel(learnedNoGood);
if (backjumpingDecisionLevel < 0) {
return ConflictAnalysisResult.UNSAT;
if (optimizeAnalysisResult) {
// Due to out-of-order assigned literals, the learned nogood may be not assigning.
backjumpingDecisionLevel = computeConflictFreeBackjumpingLevel(learnedNoGood);
if (backjumpingDecisionLevel < 0) {
return ConflictAnalysisResult.UNSAT;
}
} else {
backjumpingDecisionLevel = 0;
}
}
if (LOGGER.isTraceEnabled()) {
Original file line number Diff line number Diff line change
@@ -120,7 +120,8 @@ ConflictAnalysisResult analyzeConflictingNoGoodAndGeneraliseConflict(Antecedent
throw oops("Learned nogood is not the same as the one computed by ground analysis");
}
final ConflictAnalysisResult analysisResult = groundLearner.analyzeConflictingNoGood(violatedNoGood);
if (!additionalLearnedNoGoods.isEmpty()) {
// if backJumpLevel < 0, then problem is UNSAT (ground analysis result does additional checks for this)
if (!additionalLearnedNoGoods.isEmpty() && analysisResult.backjumpLevel >= 0) {
analysisResult.addLearnedNoGoods(additionalLearnedNoGoods);
}
return analysisResult;