Network encodings and heuristics for planning #97
Conversation
|
Hi Dan, First of all, thanks for the contributions and all the hard works (esp, I understand that rebasing is non-trivial).
|
|
Hi Soonho, I’ve fixed the warnings. I am using g++-4.9 (started after GLOG stopped working on g++-4.8). How do you want me to give you the changes? I can add to the pull request or push to your branch (mentioned below), but need access. I’m happy to discuss what I’ve done to the SAT solver. Let me know when you have time. Thanks, Dan
|
|
Hi @danbryce,
Thank you!
I'm not sure about GLOG, but we do have some issues between the JSON library and g++-4.8. I opened an issue in upstream. In the meantime, using g++-4.9 is a workaround.
I can easily cherry-pick the commit from your repository. Just let me know the commit (git SHASUM).
Thanks. I'll do that. |
https://github.com/danbryce/dreal3/feat-dan-pull-request |
|
@danbryce, thank you! |
fix(style) fix(heuristic): avoid backtracking in heuristic unless required fix(style) fix(heuristic): avoid backtracking in heuristic unless required fix(heuristic): avoid backtracking in heuristic unless required fix(style) feat(heuristics): checkpoint on implementing ode simulation feat(heuristics): checkpoint on implementing ode simulation feat(heuristics): checkpoint on implementing ode simulation feat(heuristics): checkpoint on implementing ode simulation feat(heuristics): checkpoint on implementing ode simulation feat(heuristics): checkpoint on implementing ode simulation feat(heuristics): checkpoint on implementing ode simulation feat(heuristic): ode sim heuristic cleanup
…gative -- fix(cherry-pick)
feat(heuristics): generalized time splitting heuristic feat(heuristics): generalized time splitting heuristic feat(dsolver): style
…e for CAPD parser
…tart of new planning heuristic. fix(style)
… be eliminated with prejudice
fix(CoreSMTSolver): print boolean part of model
fix(style) fix(debugging): removed unnecessary debugging
… file fix(heuristics): refactored variable selection heuristics to use common parent class and live in SMTSolver feat(.gitignore)
…red heuristic interface Forgot some new files. Fixed compiling errors caused by updated code base.
Automata instanciation Extended ile format syntax to accommodate for instanciation, network scope initialization Internal mode name encoding Initial SMT work Discrete encoding (Hopefully). Sync really took a while... Encoded benchmark (train) for k=0..2 in benchmarks/train-k*.txt Rewrote discrete mode encoding to use synchronization variables. Jump precompostion will remain an experimental feature. "Active" encoding. Added continuous encoding Renamed enforcing variable Updated train benchmark encoding in benchmarks/networked_train_testing_grounds/ Forgot to add a "maintain" for the last iteration. Changed invariant implication order Added "active" formula to the last iteration since "maintain" requires the setting of gamma variables for the flow in the final mode-space Added noop-transitions Added unused variables in transitions for value propagation (x_1_0 = x_0_t) Added dummy flows of gamma variables (gamma' = 0) to the flowmap since it's required for constructions such as x' = t * gamma Added dummy flows for variables without flows to account for the satisfaction of the goal formula (Otherwise x_final_t might be dangling) Added dumbed down generator model for testing of continuous behavior (dreach-networks/benchmarks/networked_train_testing_grounds/generator.drh Added simple model for testing discrete behavior (dreach-networks/benchmarks/networked_train_testing_grounds/discrete_test.drh) Updated benchmark outputs (dreach-networks/benchmarks/networked_train_testing_grounds/*.smt2) Changed composition parser according to mail/documentation Updated benchmarks accordingly dan's train tweaks
…de mutex constraint to encoding Added basic backwards compatability. Creation of singleton network. Fixes to the backward compatability Add option to parse the old file format to dReach runscript. Removed old, uncommented code. General clean up. Removed pathgen and possibly related stuff by mistake. Put it back in.
…ncoding mutex for goal modes. fix(cherry-pick)
fix(cherry-pick)
The current approach is to always include the encodings of the whole network. We introduce an options to change the behavior to filter out encodings of modes and related contraints, that are unreachable within k steps. Execute either the dReach runscript with the -f option, or the bmc executable with the --length_filter options. fix(style)
…assigned pure virtual
- no trailing whitespace - no tab. replace a hard-tab with 8 spaces
|
@danbryce, |
|
Yesterday, @nnarodytska and I reviewed the changes under
I think it's great and ready to be merged. At the same time, we have some questions about them:
FYI, I rebase the changes on the blessed/master and add them at https://github.com/soonhokong/dreal3/commits/feat-dan-pull-request. |
|
@4lex4nder removed this and I’ve asked him to put it back. I’ll put it in the pull request once done.
|
@danbryce, I see. Thank you! |
These are Booleans that were inferred or resolved out of the initial CNF. I need their inferred values in the output model. They are not mentioned in the “model" array or current assignment managed by the SAT solver.
This resolved an issue where the MiniSAT preprocessor was incorrectly removing Boolean variables. See issue dreal/dreal2#66. The preprocessor attempts to eliminate unfrozen variables (see SimpSMTSolver::eliminate()). There was a case where it was eliminating some pure literals and it was causing me problems. I probably need to revisit this. Freezing all booleans is safe, but might be inefficient.
If you look at CoreSMTSolver::pickBranchLit(), then you’ll see where this works. Currently, the heuristic overrides the theory suggestion. Previously, for hybrid system problems, I had the theory solver suggesting the mode paths via this interface. In my current work on planning, I needed suggestions for Booleans and thought it cleaner to remove this from the theory solver (which is unaware of Booleans). There is no reason that the theory solver cannot again make suggestions. This might be a way to implement theory propagation.
At the level of its interface, the heuristic class gets the literals (inform()), is asked for a suggestion (getSuggestion(), where it reads the trail) and backtracks (backtrack(), where it again reads the trail). It could probably remove the backtrack() method and do the necessary maintenance when asked for a suggestion next.
|
soonhokong
force-pushed
the
master
branch
2 times, most recently
from
b3bad86 to
5707f19
Compare
Tested the build and unit tests. Cherry picked only mine and Alex's commits.