Changing variable value after parsing formula
m-ajmone opened this issue · 5 comments
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().
Hi! I think what you want to do is called "restriction", i.e. you want to restrict the value of A to true. The restrict operation is directly available on each Formula. You just have to pass it an assignment telling which variables to restrict.
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.
After restricting the formula as you suggested and adding it to MiniSat, it doesn't seem to affect the assignment given by miniSat.model().
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 assignment, it still gives B as an output, even if it should've been restricted to true.
Formulas in LogicNG are immutable, so restrict returns another formula object. :)
If you pass this formula into the solver, you should get the expected result.
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.