google-deepmind / alphageometry

Apache License 2.0
4.15k stars 464 forks source link

an error of ddar #84

Open pgmthar opened 8 months ago

pgmthar commented 8 months ago

When solving this problem:

a b c = triangle a b c; d = foot d a b c; e = angle_bisector e d a c, on_line e b c; f = foot f e a c; g = intersection_ll g b f a d; h = intersection_ll h g c d f; i = on_line i e g, on_bline i g e; j = on_line j d g, on_bline j g d; k = on_line k d e, on_bline k e d; l = on_line l d i, on_line l g k; m = on_line m i k, on_bline m k i ? perp h e a b

I expected to get DD+AR failed to solve the problem., but it raised an ValueError.


Traceback (most recent call last):
  File "/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/runpy.py", line 196, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "/Library/Frameworks/Python.framework/Versions/3.10/lib/python3.10/runpy.py", line 86, in _run_code
    exec(code, run_globals)
  File "/.../alphageometry/alphageometry.py", line 657, in <module>
    app.run(main)
  File "/.../alphageometry/lib/python3.10/site-packages/absl/app.py", line 308, in run
    _run_main(main, args)
  File "/.../alphageometry/lib/python3.10/site-packages/absl/app.py", line 254, in _run_main
    sys.exit(main(argv))
  File "/.../alphageometry/alphageometry.py", line 640, in main
    run_ddar(g, this_problem, _OUT_FILE.value)
  File "/.../alphageometry/alphageometry.py", line 217, in run_ddar
    ddar.solve(g, RULES, p, max_level=1000)
  File "/.../alphageometry/ddar.py", line 95, in solve
    dervs, eq4, next_branches, added = saturate_or_goal(
  File "/.../alphageometry/ddar.py", line 50, in saturate_or_goal
    added, derv, eq4, n_branching = dd.bfs_one_level(
  File "/.../alphageometry/dd.py", line 1092, in bfs_one_level
    add = g.add_piece(name, args, deps=deps)
  File "/.../alphageometry/graph.py", line 694, in add_piece
    return self.add_perp(args, deps)
  File "/.../alphageometry/graph.py", line 1281, in add_perp
    raise ValueError(f'{ab.name} and {cd.name} Cannot be perp.')
ValueError: bc and ik Cannot be perp.
jojo23333 commented 7 months ago

I run into those too, there seems to be some bug in DDAR

tomonari-motegi commented 7 months ago

I also got the same error in DDAR. @pgmthar What is the source of this problem? I would like to know the original question and answer. I tried to prove [perp h e a b] by myself, but I couldn't solve.