Mentions légales du service

Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • rules/integraal
  • ulliana/integraal
2 results
Show changes
View open merge request
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2677 additions and 348 deletions
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSEncoder.java deleted 100644 → 0
View file @ 60f50132
package fr.boreal.explanation.solving_enumerating;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.logicalElements.api.Atom;
public interface GMUSEncoder {
EncodingResult encode(FactBase filteredGRI, Atom query);
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSProcessor.java deleted 100644 → 0
View file @ 60f50132
package fr.boreal.explanation.solving_enumerating;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.logicalElements.api.Atom;
import java.util.HashSet;
import java.util.Set;
public class GMUSProcessor {
private Set<String> gmuses = new HashSet<>();
private static final GMUSSolver solver = new GMUSSolver();
private static final GMUSTranslator translator = new GMUSTranslator();
public Set<KnowledgeBase> computeExplanations(
FactBase filteredGRI,
StaticGRIRuleTransformer staticGRIRuleTransformer,
Atom query) {
GMUSEncoder encoder = new KBtoGSATEncoder(staticGRIRuleTransformer);
var encoding = encoder.encode(filteredGRI, query);
gmuses = solver.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
return translator.translateGMUSes(gmuses, encoding.factIDMap(), encoding.ruleIDMap());
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSSolver.java deleted 100644 → 0
View file @ 60f50132
package fr.boreal.explanation.solving_enumerating;
import com.google.common.collect.BiMap;
import com.google.common.collect.HashBiMap;
import fr.boreal.model.logicalElements.api.Term;
import java.io.*;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
public class GMUSSolver {
private static final GMUSSolver INSTANCE = new GMUSSolver();
public static GMUSSolver instance() {
return INSTANCE;
}
String tmpFileName = "mus.gcnf";
File gcnfFile = new File(tmpFileName);
int timeout = 0;
public Set<String> solve(BiMap<Term, Integer> propVarIDMap,
List<List<Integer>> clauses,
int nbGroup) {
Set<String> gmuses = new HashSet<>();
writeGCNF(propVarIDMap, clauses, nbGroup);
gmuses = getGMUSes(gcnfFile);
return gmuses;
};
public void writeGCNF(BiMap<Term, Integer> propVarIDMap,
List<List<Integer>> clauses,
int nbGroup
) {
try {
FileWriter writerCNF = new FileWriter(gcnfFile, false);
writerCNF.write("p gcnf "
+ propVarIDMap.size() + " "
+ clauses.size() + " "
+ nbGroup + "\n");
for (List<Integer> clause: clauses) {
assert clause.getFirst() != null;
writerCNF.write(
"{" + clause.getFirst() + "} "
);
for (int i = 1; i < clause.size(); i++) {
assert clause.get(i) != null;
writerCNF.write(
clause.get(i) + " "
);
}
writerCNF.write(" 0\n");
}
writerCNF.close();
} catch (IOException e1) {
throw new RuntimeException("Unable to write tmp file for gcnf solver");
}
}
public Set<String> getGMUSes(File gcnfFile) {
Set<String> gmuses = new HashSet<>();
ProcessBuilder build = new ProcessBuilder().redirectErrorStream(true);
if (timeout == 0)
build.command("MARCO-MUS/marco.py", "-v", "-b", "MUSes", gcnfFile.getAbsolutePath());
else
build.command("MARCO-MUS/marco.py", "-v", "-b", "MUSes", "-s", "-T", Long.toString(timeout), gcnfFile.getAbsolutePath());
Process proc;
try {
proc = build.start();
} catch (IOException e) {
throw new RuntimeException("MARCO process ended with an error\n" + e);
}
BufferedReader in = new BufferedReader(new InputStreamReader(proc.getInputStream()));
String line;
try {
while ((line = in.readLine()) != null) {
if (line.startsWith("U")) {
gmuses.add(line.split("U ")[1]);
} else {
System.err.println(line);
}
}
} catch (IOException e) {
throw new RuntimeException("MARCO process wrote an incorrect line\n" + e);
}
proc.destroy();
return gmuses;
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/KBtoGSATEncoder.java deleted 100644 → 0
View file @ 60f50132
package fr.boreal.explanation.solving_enumerating;
import com.google.common.collect.BiMap;
import com.google.common.collect.HashBiMap;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.logicalElements.api.*;
import fr.boreal.model.logicalElements.impl.functionalTerms.GroundFunctionalTermImpl;
import fr.boreal.model.rule.api.FORule;
import java.util.*;
/**
* This class computes an encoding of explanations as GCNF formulas that can later be processed by a MUS solver
* <p>
* Ground atoms are represented as propositional variables
* <p>
* <p>
* <p>
* <p>
* 1. propVarIDmap maps a propositional variable to its corresponding (int) ID starting at 1
* 2. clauses is a list of list of integers.
* A clause take the following form:
* nbGroup, i for every atom a_i in the chase
* nbGroup, -i1, -i2, ..., i for every grounded rule a_i1 ^ a_i2 ... -> a_i
* where each integer i is the ID of a propositional variable (as stored in propVarID map)
* 3. nbGroup tracks the latest group number (starting at 0)
* <p>
* At the same time we are also computing 2 extra structures which are used in translating the GMUSes back
* to KB:
* 1. factIDmap (nbGroup - atom)
* 2. ruleIDmap (nbGroup - ungrounded rule)
*/
public class KBtoGSATEncoder implements GMUSEncoder{
StaticGRIRuleTransformer staticGRIRuleTransformer;
Predicate REL = StaticGRIRuleTransformer.REL;
public BiMap<Term, Integer> propVarIDMap = HashBiMap.create();
public BiMap<Integer, Atom> factIDMap = HashBiMap.create();
public BiMap<Integer, FORule> ruleIDMap = HashBiMap.create();
public List<List<Integer>> clauses = new ArrayList<>();
public int nbGroup = 1;
public KBtoGSATEncoder(StaticGRIRuleTransformer staticGRIRuleTransformer) {
this.staticGRIRuleTransformer = staticGRIRuleTransformer;
}
/**
* This method takes a (filtered) KB and the query and return the set of explanations.
*
* @param filteredGRI
* @param query
* @return set of explanations
*/
public EncodingResult encode(
FactBase filteredGRI,
Atom query) {
assignDefaultGroupNumberAndCreateClauseForStartQuery(query);
assignGroupNumbersAndComputeClausesForRELEdges(filteredGRI, query);
return new EncodingResult(propVarIDMap,factIDMap,ruleIDMap,clauses, nbGroup);
}
/**
* This method assigns id 1 to the query in propvarIDMap and add the query clause of group 0
* It modifies:
* 1. propvarIDMap
* 2. clauses
*
* @param query
*/
public void assignDefaultGroupNumberAndCreateClauseForStartQuery(Atom query) {
Term queryFnTermIdentifier = staticGRIRuleTransformer.createFnTermIdentifier(query);
propVarIDMap.put(queryFnTermIdentifier, propVarIDMap.size() + 1);
clauses.add(List.of(0, propVarIDMap.get(queryFnTermIdentifier) * -1));
}
/**
* This method assigns id every atom marked with REL and add a singleton group for each to clauses
* For every *relvant* REL atom a :
* (1) create a group number [nbgroup_a] for a
* (2) creates a (singleoton) clause nbgroup id_a
* It modifies:
* 1. propvarIDMap
* 2. clauses
* 3. nbGroup
* <p>
* And in the meantime it records the id of each atom to factIDMap
*
* @param filteredGRI
*/
public void assignGroupNumbersAndCreateClauseForEachSupRelAtom(FactBase filteredGRI, Atom query) {
var it = filteredGRI.getAtomsByPredicate(REL);
while (it.hasNext()) {
var relatom = it.next();
LogicalFunctionalTerm fnTermForAtom = (LogicalFunctionalTerm) relatom.getTerm(0);
Atom atom = staticGRIRuleTransformer.getAtomFromFnTerm(fnTermForAtom);
if (atom.equals(query)) {
continue;
}
propVarIDMap
.putIfAbsent(fnTermForAtom, propVarIDMap.size() + 1);
//make a group with just the atom
// TODO we may simplify this and have a single map linking the atom, the term, and the group
if (filteredGRI.contains(atom)) {
factIDMap.put(nbGroup, atom);
clauses.add(List.of(nbGroup, propVarIDMap.get(fnTermForAtom)));
}
nbGroup++;
}
}
/**
* For every *relvant* rule r :
* (1) Gives a group number [nbgroup] to every *relvant* rule r and hence to every REL_EDGE_r predicate
* (r is relevant if it is used to compute SupRel and marked by the presence of a REL_EDGE_r atom).
* <p>
* (2) Computes a set of clauses encoding the usage of r.
* Every clause is derived from an atom of the form
* REL_EDGE_r(id_grounded_body1,id_grounded_body2...,id_grounded_head)
* Every clause is encoded as a list of integers the structure
* nbgroup -id_grounded_body1 -id_grounded_body2 ... id_grounded_head
*
* @param filteredGRI
*/
public void assignGroupNumbersAndComputeClausesForRELEdges(FactBase filteredGRI, Atom query) {
Set<Predicate> allPredicatesAfterTracing = new HashSet<>();
//retrieve all predicates used to compute SupRelevant produced by the GRIBuilding and RelTracer
filteredGRI.getPredicates().forEachRemaining(predicate -> allPredicatesAfterTracing.add(predicate));
BiMap<Predicate, FORule> relEdgePredicateToRule = staticGRIRuleTransformer.getRuleToRelEdgePredicateMap().inverse();
// We compute a SET of clauses for every REL_EDGE_r *predicate*
for (Predicate relEdgePred : relEdgePredicateToRule.keySet()) {
if (allPredicatesAfterTracing.contains(relEdgePred)) {
// we compute a clause for each REL_EDGE_r *atom*
// for REL_EDGE_r(f_p(a),f_q(b)...,f_t(a)) is in SupRel we make a Horn propositional clause
// NOT f_p(a) OR NOT f_q(b) ... OR f_t(a)
// where every ground atom is a propositional variable represented by an integer
// NOT 1 OR NOT 2 ... OR K
// this is represented as a list of integers <-1 ,-2,...,K>
// and, note that as a convention, we add the group number G in the first position <G, -1 ,-2,...,K>
// records the id of each rule to ruleIDMap
ruleIDMap.put(nbGroup, relEdgePredicateToRule.get(relEdgePred));
var it = filteredGRI.getAtomsByPredicate(relEdgePred);
while (it.hasNext()) {
Atom relEdge = it.next();
Term[] atomsFnIdentifierInGroundedRule = relEdge.getTerms();
List<Integer> clause = new ArrayList<>();
clause.addFirst(nbGroup);
// adding tales
for (int i = 0; i < atomsFnIdentifierInGroundedRule.length - 1; i++) {
LogicalFunctionalTerm fnTermForAtom = (GroundFunctionalTermImpl) atomsFnIdentifierInGroundedRule[i];
Atom atom = staticGRIRuleTransformer.getAtomFromFnTerm(fnTermForAtom);
if (atom.equals(query)) {
continue;
}
propVarIDMap
.putIfAbsent(fnTermForAtom, propVarIDMap.size() + 1);
// TODO we may simplify this and have a single map linking the atom, the term, and the group
if (filteredGRI.contains(atom)) {
nbGroup++;
factIDMap.inverse().putIfAbsent(atom, nbGroup);
clauses.add(List.of(nbGroup, propVarIDMap.get(fnTermForAtom)));
}
clause.add(propVarIDMap.get(atomsFnIdentifierInGroundedRule[i]) * -1);
}
// adding tip
// TODO you have to add head atom to the dictionaries as well!
clause.add(propVarIDMap.get(atomsFnIdentifierInGroundedRule[atomsFnIdentifierInGroundedRule.length - 1])
);
clauses.add(clause);
}
}
}
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/GMUSTranslator.java → integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/marco/MARCOGMUSDecoder.java
Edit View file @ 0955fe49
package fr.boreal.explanation.solving_enumerating;
package fr.boreal.explanation.solving_enumerating.marco;
import com.google.common.collect.BiMap;
import fr.boreal.model.kb.api.FactBase;
......@@ -13,13 +13,18 @@ import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
import java.util.HashSet;
import java.util.Set;
public class GMUSTranslator {
private static final GMUSTranslator INSTANCE = new GMUSTranslator();
public static GMUSTranslator instance() {
return INSTANCE;
}
public class MARCOGMUSDecoder {
public Set<KnowledgeBase> translateGMUSes(
/**
* This method takes in the set of strings (each string represents a gmus) and the factIDMap/ruleIDMap
* and compute the set of explanations
*
* @param gmuses
* @param factIDMap
* @param ruleIDMap
* @return set of explanations
*/
public static Set<KnowledgeBase> decodeGMUSes(
Set<String> gmuses,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap
......@@ -33,8 +38,17 @@ public class GMUSTranslator {
return explanations;
}
public KnowledgeBase gmusToExpl(
/**
* This method takes in a gmus string which consists of integers separated by a space.
* Each integer is a group number.
* Then we find the element in the group and translate it back to fact or rule from the original KB.
*
* @param gmus
* @param factIDMap
* @param ruleIDMap
* @return
*/
public static KnowledgeBase gmusToExpl(
String gmus,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap) {
......
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/marco/MARCOGMUSSolver.java 0 → 100644
Edit View file @ 0955fe49
package fr.boreal.explanation.solving_enumerating.marco;
import com.google.common.collect.BiMap;
import fr.boreal.explanation.api.solver.Solver;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.logicalElements.api.Term;
import no.hasmac.jsonld.uri.Path;
import java.io.*;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
import static fr.boreal.explanation.configuration.PathFinder.ensureFilePath;
public class MARCOGMUSSolver implements Solver {
private static final MARCOGMUSSolver INSTANCE = new MARCOGMUSSolver();
public static MARCOGMUSSolver instance() {
return INSTANCE;
}
String tmpFileName = "gsat.gcnf";
File gcnfFile = new File(tmpFileName);
int timeout = 0;
/**
* This main methods call two methods:
* 1. writeGCNF: Writing the clauses to temporary gsat.gcnf file
* 2. getGMUSes: Call marco.py (marco.py MUS solver) with gsat.gcnf
* and return
*
* @param propVarIDMap
* @param clauses
* @param nbGroup
* @return gmuses
**/
public Set<String> solve(BiMap<Atom, Integer> propVarIDMap,
List<List<Integer>> clauses,
int nbGroup) {
Set<String> gmuses = new HashSet<>();
writeGCNF(propVarIDMap, clauses, nbGroup);
gmuses = getGMUSes(gcnfFile);
return gmuses;
}
;
/**
* write the temporary gsat.gcnf file
*
* @param propVarIDMap
* @param clauses
* @param nbGroup
*/
public void writeGCNF(BiMap<Atom, Integer> propVarIDMap,
List<List<Integer>> clauses,
int nbGroup
) {
System.out.println("number of clauses " + clauses.size());
try {
FileWriter writerCNF = new FileWriter(gcnfFile, false);
// the header of a gcnf file with the following format
// p gcnf + #variables + #clauses + #groups
writerCNF.write("p gcnf "
+ propVarIDMap.size() + " "
+ clauses.size() + " "
+ nbGroup + "\n");
for (List<Integer> clause : clauses) {
assert clause.getFirst() != null;
writerCNF.write(
"{" + clause.getFirst() + "} "
);
for (int i = 1; i < clause.size(); i++) {
// assert clause.get(i) != null;
writerCNF.write(
clause.get(i) + " "
);
}
writerCNF.write(" 0\n");
}
writerCNF.close();
} catch (IOException e1) {
throw new RuntimeException("Unable to write tmp file for gcnf solver");
}
}
/**
* call the external marco gmus solver
*
* @param gcnfFile
* @return
*/
public Set<String> getGMUSes(File gcnfFile) {
Set<String> gmuses = new HashSet<>();
ProcessBuilder build = new ProcessBuilder().redirectErrorStream(true);
String command;
if (timeout == 0)
build.command(ensureFilePath("integraal-explanation/MARCO-MUS/marco.py", "MARCO-MUS/marco.py"), "-v", "-b", "MUSes", gcnfFile.getAbsolutePath(), " -a");
else
build.command(ensureFilePath("integraal-explanation/MARCO-MUS/marco.py", "MARCO-MUS/marco.py"), "-v", "-b", "MUSes", "-T", Long.toString(timeout), gcnfFile.getAbsolutePath(), " -a");
Process proc;
try {
proc = build.start();
} catch (IOException e) {
System.out.println("Was not able to run MARCO locally, trying now with Docker\n" + e);
return getGMUSesDocker(gcnfFile);
}
BufferedReader in = new BufferedReader(new InputStreamReader(proc.getInputStream()));
String line;
try {
while ((line = in.readLine()) != null) {
System.out.println(line);
if (line.startsWith("Traceback (most recent call last)")) {
System.out.println("Locally installed MARCO had an execution error. Trying to see if the docker-image is active. \n");
return getGMUSesDocker(gcnfFile);
}
if (line.startsWith("U")) {
gmuses.add(line.split("U ")[1]);
System.out.println(line);
} else {
if (line.startsWith("S")) {
// satisfiable set
System.out.println(line);
} else {
System.err.println(line);
}
}
}
} catch (IOException e) {
throw new RuntimeException("MARCO process wrote an incorrect line\n" + e);
}
proc.destroy();
return gmuses;
}
/**
* call marco via docker
*
* @param gcnfFile
* @return
*/
public Set<String> getGMUSesDocker(File gcnfFile) {
Set<String> gmuses = new HashSet<>();
ProcessBuilder build = new ProcessBuilder().redirectErrorStream(true);
gcnfFile = gcnfFile.getAbsoluteFile();
File parentDir = gcnfFile.getParentFile();
if (parentDir == null) {
throw new RuntimeException("Error: File " + gcnfFile.getAbsolutePath() + " has no parent directory.");
}
// 🔹 Use Docker to run MARCO instead of calling "MARCO-MUS/marco.py" directly
if (timeout == 0) {
build.command(
"docker", "run", "--rm", "--init",
"-v", parentDir.getAbsolutePath() + ":/app/tests",
"marco-image", "-v", "-b", "MUSes", "-s", "/app/tests/" + gcnfFile.getName()
);
build.command(
"docker", "run", "--rm", "--init",
"-v", gcnfFile.getParentFile().getAbsolutePath() + ":/app/tests",
"marco-image", "-v", "-b", "MUSes", "-s", "/app/tests/" + gcnfFile.getName()
);
} else {
build.command(
"docker", "run", "--rm", "--init",
"-v", gcnfFile.getParentFile().getAbsolutePath() + ":/app/tests",
"marco-image", "-v", "-b", "MUSes", "-s", "-T", Long.toString(timeout), "/app/tests/" + gcnfFile.getName()
);
}
Process proc;
try {
proc = build.start();
} catch (IOException e) {
throw new RuntimeException("Was not able to run MARCO with Docker" + e);
}
// 🔹 Read MARCO's output from Docker
BufferedReader in = new BufferedReader(new InputStreamReader(proc.getInputStream()));
String line;
try {
while ((line = in.readLine()) != null) {
//System.out.println(line);
if (line.startsWith("U")) {
gmuses.add(line.split("U ")[1]);
System.out.println(line);
} else {
if (line.startsWith("S")) {
// satisfiable set
System.out.println(line);
} else {
System.err.println(line);
}
}
}
} catch (IOException e) {
throw new RuntimeException("MARCO process returned an incorrect line\n" + e);
}
// 🔹 Ensure process is terminated properly
try {
int exitCode = proc.waitFor();
if (exitCode != 0) {
throw new RuntimeException("MARCO process exited with code " + exitCode);
}
} catch (InterruptedException e) {
Thread.currentThread().interrupt();
throw new RuntimeException("MARCO execution interrupted\n" + e);
}
return gmuses;
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/GMUSStatistics.java 0 → 100644
Edit View file @ 0955fe49
package fr.boreal.explanation.solving_enumerating.sat4j;
public class GMUSStatistics {
public int heuristicsDetectedNoConflictingClauseExistsWithinTheGroups = 0;
public int savedByHeuristicsOne = 0;
public int heuristicsDetectedThatNoneOfTheAlternativesCanBeProved = 0;
public int notSavedByHeuristics = 0;
public long sat4jCallTime = -1;
public long inteGraalToSat4JClauseConversion = -1;
public long sat4jToInteGraalMUSDecoding = -1;
public int heuristicsDetectedNonMinimalityFromSameGroupClauseConflict = 0;
public int heuristicsDetectedSameClauseInDifferentGroup = 0;
public int usedHeavyChaseBasedCheckToDiscoverNonMinimality = 0;
public int theConflictingClauseCannotBeInferredAsItHasNoSupportAtomClause = 0;
public int heuristicDetectedAPreviousGroupMUSWithLessGroupsThanTheCandidateGMUS = 0;
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/HornClauses.java 0 → 100644
Edit View file @ 0955fe49
package fr.boreal.explanation.solving_enumerating.sat4j;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
public class HornClauses {
/**
* A record to hold the two groups of supporting clauses:
* - size2Clauses: clauses that have exactly 2 elements.
* - sizeGreaterClauses: clauses that have more than 2 elements.
*/
public record SupportingClausesResult(
List<List<Integer>> size2Clauses,
List<List<Integer>> sizeGreaterClauses
) {
List<List<Integer>> getAllClauses() {
List<List<Integer>> allClauses = new ArrayList<>();
allClauses.addAll(size2Clauses);
allClauses.addAll(sizeGreaterClauses);
return allClauses;
}
}
/**
* Retrieves all clauses (other than the given clause) from theory that
* can directly or indirectly prove a propositional variable in the body of c.
* <p>
* In this representation:
* - clause.get(0) is the group number,
* - clause.subList(1, clause.size()-1) are the body literals,
* - clause.get(clause.size()-1) is the head literal.
*
* @param clause The clause for which supporting clauses are sought.
* @param theory The list of all group SAT clauses.
* @return A record with two components:
* - size2Clauses: the list of supporting clauses of size 2.
* - sizeGreaterClauses: the list of supporting clauses of size greater than 2.
*/
public SupportingClausesResult getSupportingClauses(List<Integer> clause, List<List<Integer>> theory) {
// Collect all supporting clauses first.
List<List<Integer>> result = new ArrayList<>();
Set<List<Integer>> visitedClauses = new HashSet<>();
// Ensure the clause has a body: must have more than just group number and head.
if (clause.size() <= 2) {
return new SupportingClausesResult(new ArrayList<>(), new ArrayList<>());
}
// For each literal in the body (indexes 1 to clause.size()-2)
for (int var : clause.subList(1, clause.size() - 1)) {
findSupportingClauses(var * -1, theory, result, visitedClauses, clause);
}
// Split the results based on clause size.
List<List<Integer>> size2Clauses = new ArrayList<>();
List<List<Integer>> sizeGreaterClauses = new ArrayList<>();
for (List<Integer> c : result) {
if (c.size() == 2) {
size2Clauses.add(c);
} else if (c.size() > 2) {
sizeGreaterClauses.add(c);
}
}
return new SupportingClausesResult(size2Clauses, sizeGreaterClauses);
}
/**
* Recursively finds and adds all clauses that can prove the given variable.
*
* @param var The propositional variable to be proven.
* @param theory The list of all group SAT clauses.
* @param result The running list of supporting clauses.
* @param visited A set of clauses that have already been processed (to avoid cycles).
* @param originalClause The clause for which we are finding supporting clauses.
*/
private void findSupportingClauses(int var, List<List<Integer>> theory, List<List<Integer>> result,
Set<List<Integer>> visited, List<Integer> originalClause) {
for (List<Integer> candidate : theory) {
// Skip the original clause or any clause already processed.
if (candidate == originalClause || visited.contains(candidate)) {
continue;
}
// Candidate's head literal is at the last index.
if (candidate.get(candidate.size() - 1) == var) {
result.add(candidate);
visited.add(candidate);
// If the candidate has a body (i.e. size > 2), search recursively.
if (candidate.size() > 2) {
for (int bodyVar : candidate.subList(1, candidate.size() - 1)) {
findSupportingClauses(bodyVar * -1, theory, result, visited, originalClause);
}
}
}
}
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/solving_enumerating/sat4j/Sat4JTranslator.java 0 → 100644
Edit View file @ 0955fe49
package fr.boreal.explanation.solving_enumerating.sat4j;
import com.google.common.collect.BiMap;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.kb.api.RuleBase;
import fr.boreal.model.kb.impl.KnowledgeBaseImpl;
import fr.boreal.model.kb.impl.RuleBaseImpl;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.rule.api.FORule;
import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
import java.util.HashSet;
import java.util.List;
import java.util.Set;
public class Sat4JTranslator {
/**
* This method takes in the set of strings (each string represents a gmus) and the factIDMap/ruleIDMap
* and compute the set of explanations
*
* @param gmuses
* @param factIDMap
* @param ruleIDMap
* @return set of explanations
*/
public static Set<KnowledgeBase> decodeGMUSes(
List<List<List<Integer>>> gmuses,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap
) {
Set<KnowledgeBase> explanations = new HashSet<>();
for (var gmus : gmuses) {
explanations.add(gmusToExpl(gmus, factIDMap, ruleIDMap));
}
return explanations;
}
/**
* This method takes in a gmus string which consists of integers separated by a space.
* Each integer is a group number.
* Then we find the element in the group and translate it back to fact or rule from the original KB.
*
* @param gmus
* @param factIDMap
* @param ruleIDMap
* @return
*/
public static KnowledgeBase gmusToExpl(
List<List<Integer>> gmus,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap) {
FactBase explFB = new SimpleInMemoryGraphStore();
RuleBase explRB = new RuleBaseImpl();
for (var clause : gmus) {
int nbGroup = clause.getFirst();
if (nbGroup > 0) {
if (factIDMap.containsKey(nbGroup)) {
explFB.add(factIDMap.get(nbGroup));
} else if (ruleIDMap.containsKey(nbGroup)) {
explRB.add(ruleIDMap.get(nbGroup));
}
}
}
KnowledgeBase expl = new KnowledgeBaseImpl(explFB, explRB);
return expl;
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/GRI/dynamicProcessing/RELTracer.java → integraal/integraal-explanation/src/main/java/fr/boreal/explanation/to_be_removed/GRI/dynamicProcessing/RELTracer.java
Edit View file @ 0955fe49
package fr.boreal.explanation.GRI.dynamicProcessing;
package fr.boreal.explanation.to_be_removed.GRI.dynamicProcessing;
import fr.boreal.explanation.configuration.DefaultChaseForExplanations;
import fr.boreal.explanation.ruleFactories.StaticGRIRuleTransformer;
import fr.boreal.explanation.kb_gri.rule_transformation.GRIRuleTransformer;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.kb.impl.KnowledgeBaseImpl;
......@@ -12,7 +12,7 @@ import org.slf4j.Logger;
import org.slf4j.LoggerFactory;
/**
* This class is used to compute all relevant atoms for a given query.
* This class is used to compute all relevant bodyAtoms for a given query.
*/
public class RELTracer {
......@@ -26,12 +26,12 @@ public class RELTracer {
*/
public FactBase computeQueryRelevant(
KnowledgeBase gri,
StaticGRIRuleTransformer ruleTransformerFactory,
Atom query) {
//TODO : modify and add the dynamic rules
gri = new KnowledgeBaseImpl(new SimpleInMemoryGraphStore(gri.getFactBase().getAtomsInMemory()), gri.getRuleBase());
//first, check that the query is entailed
Atom queryWithFuncId = ruleTransformerFactory.createAtomWithStoredFnTermIdentifier(query);
Atom queryWithFuncId = GRIRuleTransformer.instance().createAtomWithStoredFnTermIdentifier(query);
if (!gri.getFactBase().contains(queryWithFuncId)) {
LOG.warn("Query " + query + " not entailed by the input KB.");
......@@ -39,7 +39,7 @@ public class RELTracer {
}
// add seed atom to the factbase
Atom RELquery = new AtomImpl(StaticGRIRuleTransformer.REL, StaticGRIRuleTransformer.instance().createFnTermIdentifier(query));
Atom RELquery = new AtomImpl(GRIRuleTransformer.REL, GRIRuleTransformer.createFnTermIdentifier(query));
gri.getFactBase().add(RELquery);
//propagate REL and REL_EDGE
......
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/to_be_removed/GRI/fallback/AllMUSesExample.java 0 → 100644
Edit View file @ 0955fe49
package fr.boreal.explanation.to_be_removed.GRI.fallback;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.tools.AllMUSes;
public class AllMUSesExample {
public static void main(String[] args) {
// Initialize AllMUSes with the default solver
AllMUSes allMUSes = new AllMUSes(SolverFactory.instance());
// Get solver instance
ISolver solver = allMUSes.getSolverInstance();
solver.newVar(3); // Declare enough variables
// List to store clauses
List<IVecInt> clauseList = new ArrayList<>();
// Map to store readable clause representations
Map<Integer, String> clauseDescriptions = new HashMap<>();
try {
clauseDescriptions.put(1, "(A -> B)");
IVecInt clause1 = new VecInt(new int[]{-1,2});
solver.addClause(clause1);
clauseList.add(clause1);
clauseDescriptions.put(2, "(A)");
IVecInt clause2 = new VecInt(new int[]{1});
solver.addClause(clause2);
clauseList.add(clause2);
clauseDescriptions.put(3, "(¬B)");
IVecInt clause3 = new VecInt(new int[]{-2});
solver.addClause(clause3);
clauseList.add(clause3);
clauseDescriptions.put(4, "(C -> B)");
IVecInt clause4 = new VecInt(new int[]{-3,2});
solver.addClause(clause4);
clauseList.add(clause4);
clauseDescriptions.put(5, "(C)");
IVecInt clause5 = new VecInt(new int[]{3});
solver.addClause(clause5);
clauseList.add(clause5);
// Debugging: Print problem structure
System.out.println("Total Variables: " + solver.nVars());
System.out.println("Total Clauses: " + solver.nConstraints());
// Compute all MUSes
List<IVecInt> muses = allMUSes.computeAllMUSes();
// Print MUSes with readable clause descriptions
System.out.println("\nMinimal Unsatisfiable Subsets (MUSes) found:");
for (IVecInt mus : muses) {
System.out.print("{ ");
for (int i = 0; i < mus.size(); i++) {
int clauseIndex = mus.get(i);
System.out.print(clauseDescriptions.getOrDefault(clauseIndex, "Unknown") + " ");
}
System.out.println("}");
}
} catch (ContradictionException e) {
System.out.println("Contradiction found while adding clauses.");
}
}
}
integraal/integraal-explanation/src/main/java/fr/boreal/explanation/tracker_gri/encoders/GSATEncodingResult_TrackerGRI.java 0 → 100644
Edit View file @ 0955fe49
package fr.boreal.explanation.tracker_gri.encoders;
import com.google.common.collect.BiMap;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.logicalElements.api.Term;
import fr.boreal.model.rule.api.FORule;
import java.util.List;
/**
*
* @param propVarIDMap map from propositional variables to integers
* @param factIDMap map from bodyAtoms to integers
* @param ruleIDMap maps from rules to integers
* @param clauses encoded GSAT
* @param nbGroup number of groups in the GSAT
*/
public record GSATEncodingResult_TrackerGRI(BiMap<Atom, Integer> propVarIDMap,
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap,
List<List<Integer>>clauses, int nbGroup) {}