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
Changing variable value after parsing formula #25
Comments
Hi! I think what you want to do is called "restriction", i.e. you want to restrict the value of final FormulaFactory f = new FormulaFactory();
final Formula formula = f.parse("A & ~(B | ~C)");
final Assignment assignment = new Assignment(true);
assignment.addLiteral(f.variable("A")); // --> A is assigned to true
final Formula restrictedFormula = formula.restrict(assignment);
System.out.println(restrictedFormula); // returns "~(B | ~C)" |
Thanks for the answer, but I'm not sure why it is still not working. final Formula formula = p.parse("A & ~(B | ~C)");
Assignment assignmentTest = new Assignment(true);
assignmentTest.addLiteral(f.variable("B"));
formula.restrict(assignmentTest);
final SATSolver miniSat = MiniSat.miniSat(f);
miniSat.add(formula);
final Assignment assignment = miniSat.model(); When listing the negatives of |
Formulas in LogicNG are immutable, so I edited my example above to make it clearer. |
Alternatively you could add the restrictions directly to the solver: final FormulaFactory f = new FormulaFactory();
final Formula formula = f.parse("A & ~(B | ~C)");
final SATSolver solver = MiniSat.miniSat(f);
solver.add(formula);
solver.add(f.variable("A"));
solver.sat();
final Assignment model = solver.model(); // contains A positively |
Thank you very much, solved. |
Hello, I was wondering if there's a way to change a variable's value after parsing a formula, for example:
After parsing ("A & ~(B | ~C)"), is there a way to give "A" the value "true", and then solve it?
In other words, to only get the assignments where A is true, without using enumerateAllModels().
The text was updated successfully, but these errors were encountered: