Draft:Geometric constraint solving: Difference between revisions

Revision as of 21:50, 29 January 2021

Revision as of 00:21, 3 March 2021

Line 1:

= Introduction<ref>Sitharam, M., John, A. S., & Sidman, J. (2018). Handbook of Geometric Constraint Systems Principles. Chapman and Hall/CRC</ref><ref>Bouma, W., Fudos, I., Hoffmann, C., Cai, J., & Paige, R. (1995). Geometric constraint solver. Computer-Aided Design, 27(6), 487-501.</ref> =

The goal of the geometric constraint solver is to find one or more solutions of GCS. The solver also should be able to report if there is no solution. The solver can be tolerated to report no solution but actually there is at least one solution ([https://en.wikipedia.org/wiki/False_positives_and_false_negatives[False positives and false negatives#False_negative_errorFalse negative error|false negative]]). However, it is not allowed to provide a solution that does not exist ([https://en.wikipedia.org/wiki/False_positives_and_false_negatives[False positives and false negatives#False_positive_errorFalse positive error|false positive]]).

Given a [[Geometric Constraint System|geometric constraint system]] (GCS) with <math>n</math> equality constraints, we seek approaches for finding solutions (realizations) or structural characterization of GCS based on the properties of the resulting set of geometrically constrained configurations or realizations. A realization of GCS is the set of zero(es) of the corresponding algebraic system. The [[Geometric Constraint System#Definitions|genericity of a GCS]] is important to know before finding the solutions. Whether a system is [[Geometric Constraint System#Definitions|generic]] determines which type of solvers we can use. It is called generic when each of the variables in a system has approximate [https://en.wikipedia.org/wiki/Degrees_of_freedom_(mechanics) degree-of-freedom] and each [https://en.wikipedia.org/wiki/Constraint_(mathematics) constraint] corresponds to at least one equation.<ref>Sitharam, M., & Zhou, Y. (2004). Mixing features and variational constraints in 3d. CAD, available upon request.</ref> The property of a generic system is well-behaved that we can use both [[#Combinatorial Approaches|combinatorial]] and [[#Algebraic & Automated Geometry Theorem Proving Methods|algebraic algorithm]] to solve it. However, in some special cases, the assignments of variables such as length and angle in equations mapped to the same underlying graph may give different classifications. We categorize a system as [[Geometric Constraint System#Definitions|non-generic]] if it has these nonideal properties. Only [[#Algebraic & Automated Geometry Theorem Proving Methods|algebraic methods]] are able to solve non-generic systems since they are not structural (combinatorial).

Given a [[Geometric Constraint System|geometric constraint system]] (GCS) with <math>n</math> equality constraints, we seek approaches for finding solutions (realizations) or structural characterization of GCS based on the properties of the resulting set of geometrically constrained configurations or realizations. A realization of GCS is the set of zero(es) of the corresponding algebraic system. The [[Geometric Constraint System#Definitions|genericity of a GCS]] is important to know before finding the solutions. Whether a system is [[Geometric Constraint System#Definitions|generic]] determines which type of solvers we can use. It is called generic when each of the variables in a system has approximate [https://en.wikipedia.org/wiki/Degrees_of_freedom_[Degrees of freedom (mechanics) |degree-of-freedom]] and each [https://en.wikipedia.org/wiki/Constraint_[Constraint (mathematics) |constraint]] corresponds to at least one equation.<ref>Sitharam, M., & Zhou, Y. (2004). Mixing features and variational constraints in 3d. CAD, available upon request.</ref> The property of a generic system is well-behaved that we can use both [[#Combinatorial Approaches|combinatorial]] and [[#Algebraic & Automated Geometry Theorem Proving Methods|algebraic algorithm]] to solve it. However, in some special cases, the assignments of variables such as length and angle in equations mapped to the same underlying graph may give different classifications. We categorize a system as [[Geometric Constraint System#Definitions|non-generic]] if it has these nonideal properties. Only [[#Algebraic & Automated Geometry Theorem Proving Methods|algebraic methods]] are able to solve non-generic systems since they are not structural (combinatorial).

Given a graph <math>G</math> with constraints <math>C</math>, we can ask GCS problems as follow and solve them separately:

''' Does GCS have at least one real realization and is it a generic or non-generic system?'''

Line 20 ⟶ 18:

'''- Yes, it has an infinite number set of solutions ([[Geometric Constraint System#Definitions|under-constrained]]).'''

<br>Generic system → Add more constraint edges to make the graph rigid.

<br>Non-generic system → Use [https://en.wikipedia.org/wiki/Configuration_space_[Configuration space (mathematics) |configuration space]]<ref>Sitharam, M., & Gao, H. (2010). Characterizing graphs with convex and connected cayley configuration spaces. Discrete & Computational Geometry, 43(3), 594-625.</ref> to describe the solution space.

The geometric constraint solvers can be classified into three categories: 1) [[#Algebraic & Automated Geometry Theorem Proving Methods|algebraic & automated geometry theorem proving methods]]; 2) [[#Combinatorial-Algebraic Algorithm|combinatorial-algebraic algorithm]] and 3) [[#Combinatorial Approaches|combinatorial algorithm]]. The algebraic-based solvers treat GCS as a [https://en.wikipedia.org/wiki/System_of_polynomial_equations [system of polynomial equations]] and solve it algebraically in either synthetic or algebraic form. The combinatorial algorithm leverages geometric properties of structure such as [[Geometric_Rigidity:_Theorems|rigidity theorems]] to find the realization. At last, the combinatorial-algebraic methods are the hybrid of the former two types of methods.

The geometric constraint solvers can be classified into three categories: 1) [[#Algebraic & Automated Geometry Theorem Proving Methods|algebraic & automated geometry theorem proving methods]]; 2) [[#Combinatorial-Algebraic Algorithm|combinatorial-algebraic algorithm]] and 3) [[#Combinatorial Approaches|combinatorial algorithm]]. The algebraic-based solvers treat GCS as a [https://en.wikipedia.org/wiki/System_of_polynomial_equations system of polynomial equations] and solve it algebraically in either synthetic or algebraic form. The combinatorial algorithm leverages geometric properties of structure such as [[Geometric_Rigidity:_Theorems|rigidity theorems]] to find the realization. At last, the combinatorial-algebraic methods are the hybrid of the former two types of methods.

= Algebraic & Automated Geometry Theorem Proving Methods<ref>Chou, S. C., Gao, X. S., & Zhang, J. Z. (1996). Automated generation of readable proofs with geometric invariants. Journal of Automated Reasoning, 17(3), 325-347.</ref> =

<!-- Instructor: Combine Algebraic with Automated Geometry Theorem Proving Methods -->

Solving a geometric constraint problem is equivalent to [[Automated Geometry Theorem Proving|automated geometry theorem proving]]. Mathematicians have started using computers proving math theory in the mid-20 century. Even though the capacity and computing power is limited at the beginning, computer-assisted proving technique has verified many mathematical theorems never proved by the human in history. [https://en.wikipedia.org/wiki/Proof_by_exhaustion [Proof by exhaustion]] is the principle of automated geometry theorem proving. Given a mathematical theorem, the computer tests if the theorem hold for all the possible cases. Automated geometry theorem proving demonstrates its versatile ability being used in different fields such as [https://en.wikipedia.org/wiki/Mathematics_education[Mathematics education|mathematic education]] [https://en.wikipedia.org/wiki/[Computer-aided_designaided design|CAD]], [https://en.wikipedia.org/wiki/[Robotics |robotic]], [https://en.wikipedia.org/wiki/Computer_vision [computer vision]], and [https://en.wikipedia.org/wiki/Artificial_intelligence [artificial intelligence]].

[[Automated Geometry Theorem Proving|automated geometry theorem proving]] can be classified into three types based on the different foundations: algebraic, synthetic, semi-synthetic, and numerical.

== Synthetic Form ==

[[Automated Geometry Theorem Proving#Synthetic Methods|synthetic method]] does not use coordinates and algebraic formula for representing geometric statements. Instead, it proves theorems by leveraging geometric properties e.g. [https://en.wikipedia.org/wiki/Triangle_inequality [triangle inequality]] and [https://en.wikipedia.org/wiki/Pythagorean_theorem[Pythagorean theorem|Pythagoras theorem]]. Therefore, the synthetic method is able to produce human-readable proof. The synthetic method is also called the axiom method since it usually adds auxiliary elements when considering the configuration. Sometimes the tremendous number of auxiliary elements can cause a [https://en.wikipedia.org/wiki/Combinatorial_explosion [combinatorial explosion]] in search space. Thus, developing a proper hierarchy of construction to reduce the unnecessary step is a challenging problem in the synthetic method. Note that geometric properties can be represented as bunches of math equations, so it is practicable to convert synthetic methods into algebraic methods.

There are many automated theorem-proving programs using [[synthetic method]]; for example, Geometry Machine<ref>Gelernter, H., Hansen, J. R., & Loveland, D. W. (1960, May). Empirical explorations of the geometry theorem machine. In Papers presented at the May 3-5, 1960, western joint IRE-AIEE-ACM computer conference (pp. 143-149).</ref> is one of the first automated reasoning systems. After that, the researchers proposed GRAMY<ref>Matsuda, N., & Vanlehn, K. (2004). Gramy: A geometry theorem prover capable of construction. Journal of Automated Reasoning, 32(1), 3-33.</ref> and iGeoTutor<ref>Wang, K., & Su, Z. (2015, June). Automated geometry theorem proving for human-readable proofs. In Twenty-Fourth International Joint Conference on Artificial Intelligence.</ref> based on the deductive database method. Moreover, the logic-based methods are also developed to prove the geometrics theorems such as ArgoCLP<ref>Stojanović, S., Pavlović, V., & Janičić, P. (2010, July). A coherent logic based geometry theorem prover capable of producing formal and readable proofs. In International Workshop on Automated Deduction in Geometry (pp. 201-220). Springer, Berlin, Heidelberg.</ref> and OTTER<ref>Beeson, M., & Wos, L. (2014, July). OTTER proofs in Tarskian geometry. In International Joint Conference on Automated Reasoning (pp. 495-510). Springer, Cham.</ref>

Line 43 ⟶ 40:

=== Area Methods ===

The area method uses geometric quantities to prove many more complex theorems such as [https://en.wikipedia.org/wiki/[Varignon%27s_theorem27s theorem|Varignon’s theorem]] and [https://en.wikipedia.org/wiki/[Pascal%27s_theorem27s theorem|Pascal's theorem]].

<!--

The geometric quantities used in this method are all area-based. The mathematics also extend the research of the area method to solid Euclidean[] and non-Euclidean geometries[] combining with Collins algorithm[] for solving a geometric inequality system[].

Line 49 ⟶ 46:

-->

=== Full-angle Methods ===

The principle of the full-angle method is analogy to the area method. The only difference is the geometric quantities it used are angle-based. The full-angle method can prove plenty of non-trivial theorems such as [https://en.wikipedia.org/wiki/Simson_line[Simson line|Simson’s theorem]], [https://en.wikipedia.org/wiki/[Miquel%27s_theorem27s theorem|Miquel's theorem]], and [https://en.wikipedia.org/wiki/Five_circles_theorem[Five circles theorem|Five circle theorem]].

<!--

Such as [[inscribed angle theorem]], inscribed angles subtended by the same arc are equal; one property of [[transversal geometric]], if <math>\overline{PX}</math> is parallel to <math>\overline{UV}</math> , then <math>\angle[AB, PX] = \angle[AB, UV]</math>.

-->

=== Vector-based Methods <ref>Chou, S. C., Gao, X. S., & Zhang, J. Z. (1993, August). Automated geometry theorem proving by vector calculation. In Proceedings of the 1993 international symposium on Symbolic and algebraic computation (pp. 284-291).</ref> ===

As the name implies, vector-based method use geometry quantities related to vectors for the proof such as the linearity property of the [https://en.wikipedia.org/wiki/Inner_product_space[Inner product space|inner product]]. Some more complex theorem such as the [https://en.wikipedia.org/wiki/Altitude_[Altitude (triangle)#Orthocenter |Orthocenter theorem]] and [https://en.wikipedia.org/wiki/[Cantor%27s_theorem27s theorem|Cantor's Theorem]] can be proved by vector-based methods.

<!--

, <math>\langle \alpha A + \beta B, C\rangle = \alpha \langle A, C\rangle + \beta \langle B, C \rangle</math>, and conjugate symmetry property, <math>\langle A, B \rangle = -\langle B,A \rangle</math>.

Line 63 ⟶ 60:

=== Mass-Point Methods ===

The mass-point method directly utilizes geometric points instead of geometric quantities. The properties of the [https://en.wikipedia.org/wiki/Barycentric_coordinate_system[Barycentric coordinate system|barycentric point]] are used as the proposition for the proofs. Many geometric statements can be proved by mass-point methods including [https://en.wikipedia.org/wiki/[Pappus%27s_centroid_theorem27s centroid theorem|Pappus' theorem]] and

[https://en.wikipedia.org/wiki/Butterfly_theorem[Butterfly theorem|Butterfly Theorem]] for quadrilaterals.

<!--

Some examples of barycentric point properties: 1) <math> xAB = yPQ \;\; iff \;\; xA - xB = yP - yQ</math>; 2) Any point <math>P</math> on plane <math>ABC</math> can be expressed as the linear combination of <math>A</math>, <math>B</math>, <math>C</math> uniquely in the form <math>P = aA + bB + (1-a-b)C</math>.

Line 70 ⟶ 67:

== Algebraic Form ==

The [[Automated Geometry Theorem Proving#Algebraic Methods|algebraic method]] translates the representation of geometric statements into a [https://en.wikipedia.org/wiki/Nonlinear_system[Nonlinear system|system of nonlinear equations]]. The solutions can be obtained by solving a system of equations with nonlinear equation solvers. The algebraic method has the advantages of generality, dimension independent, and all synthetics methods also can be translated into algebraic form. However, the major drawback is that it is unable to generate human-readable proofs. Moreover, some procedures in the proofs do not have any geometric synthetic meaning.

=== Numerical Methods ===

The [https://en.wikipedia.org/wiki/Numerical_analysis[Numerical analysis|numerical method]] translates geometric constraints into algebraic linear or non-linear equations. Then using numerical methods such as [https://en.wikipedia.org/wiki/[Newton%27s_method27s method|Newton-Raphson]], [https://en.wikipedia.org/wiki/Lagrange_polynomial[Lagrange polynomial|Lagrange interpolation polynomial]], and [https://en.wikipedia.org/wiki/Gaussian_elimination [Gaussian elimination]] to approach the solution.

=== Symbolic Methods ===

The symbolic methods such as [https://en.wikipedia.org/wiki/[Buchberger%27s_algorithm27s algorithm|Buchberger]] and [[Automated Geometry Theorem Proving#Algebraic Methods|Wu-Ritt]] are able to compute the [https://en.wikipedia.org/wiki/[Gr%C3%B6bner_basisB6bner basis|Gröbner basis]] with a given system of equations. These methods map the system of polynomial equations to a triangular system, this procedure also called [https://en.wikipedia.org/wiki/Triangular_matrix[Triangular matrix#Triangularisability |triangularization]]. The solution of the triangular system is equivalent to the given system and can be solved in exponential running time. On the other hand, the author Kondo utilizes [https://en.wikipedia.org/wiki/[Buchberger%27s_algorithm27s algorithm|Buchberger's Algorithm]] to formulate polynomial equations that can record the addition and deletion of constraints.

<!--Instructor: This should go under Algebraic Methods-->

=== Coordinate-Free Method ===

The coordinate-free methods are the solvers for [https://en.wikipedia.org/wiki/Incidence_geometry [incidence geometry]]. The geometry theorems are called incidence geometry which solves the incident properties between geometric elements such as line circle intersects problems. The feature of incidence geometry is pure qualitative without measurement. Bracket algebra<ref>Sidman, J. & Traves, W. Cayley Factorizationandspecial Positions. In: Sitharaman, M., St.John, A., and Sidman, J. (ed.), Handbook of Geometric Constraints Systems: Principles.</ref> and [https://en.wikipedia.org/wiki/[Grassmann%E2%80%93Cayley_algebra93Cayley algebra|Grassmann-Cayley algebra]] are the standard treatments in coordinate-free methods for dealing with incidence statements and constructions.

= Combinatorial-Algebraic Algorithm =

Combinatorial-algebraic algorithms aim at solving graph-based problems. In graph-based problem, given a [https://en.wikipedia.org/wiki/Graph_[Graph (discrete_mathematicsdiscrete mathematics)#Undirected_graphUndirected graph|undirected graph]] <math> G = (V, E) </math> sitting on top of a framework, where the nodes <math>V</math> represent the geometric elements and the edges denote the constraints. When the numbers of geometric elements <math>|V|</math> and constraints <math>|E|</math> are low, it is possible to directly translate the graph into algebraic form with a system of polynomial equations. However, with a more complex graph, the growth of the number of geometric elements and constraints makes the pure algebraic methods no longer practical. The combinatorial-algebraic algorithm breaks the system into several subsystems and solves them separately, then combine the solutions from each subsystem into the solution for the entire system. The solving time for the combinatorial-algebraic algorithm is much faster than the pure algebraic method when solving complex graph-based problems. This is because the solving time increases exponentially along with the number of variables. And combinatorial-algebraic algorithms only need to solve subsystems with much fewer variables than the whole system.

The combinatorial-algebraic algorithm can be classified into [[Decomposition Recombination Planning|decomposition recombination planning (DR-planning)]] and [[#Propagation Method|propagation method]].

Line 97 ⟶ 94:

[[Tree/ Triangle Decomposable Graphs|Triangle decomposition]] method as known as tree decomposition works on a graph built from constraint equations. The tree decomposition methods can be categorized as a top-down and bottom-up approach. The top-down method views GCS as several independently solvable subsystems. After the solutions for each subsystem have been solved, those solutions can be combined into new constrains for solving the remaining unsolved GCS at a higher level. Similarly, the decomposition can also be done by bottom-up, where the triples of solved geometric objects seek pairwise that shares a geometric primitive.

Owen's graph analysis<ref>Owen, J. C. (1991, May). Algebraic solution for geometry from dimensional constraints. In Proceedings of the first ACM symposium on Solid modeling foundations and CAD/CAM applications (pp. 397-407).</ref> is the pioneer of the top-down method which decomposes the constraint graph into smaller [https://en.wikipedia.org/wiki/SPQR_tree[SPQR tree|tri-connected components]]. Then, recursively split the graph into three subgraphs by cutting at articulation vertices. The triangles in each subgraph correspond to the system of quadratic equations that easy to be solved. Bouma's method is the first bottom-up decomposition approach. It first finds the triangles with solvable subsystems in the graph then combines the solutions the same with the top-down approach. The bottom-up approach has the advantage of detecting over-constrained subgraphs.

==== Maximum Matching-based Decomposition ====

Similar to the algorithms for detecting [[Geometric Rigidity: Theorems|rigidity of framework]]. This type of DR-planning algorithm performs [[Decomposition Recombination Planning#Types of Decomopsition|maximum matching]] on [https://en.wikipedia.org/wiki/Bipartite_graph[Bipartite graph|bipartite graphs]] to generate the DR-plan. Such algorithms include [https://en.wikipedia.org/wiki/[Dulmage%E2%80%93Mendelsohn_decomposition93Mendelsohn decomposition|Dulmage-Mendelsohn Decomposition]] and Assur Decomposition<ref>Assur, L. V., & Artobolevskij, I. I. (1952). Issledovanie ploskih steržnevyh mehanizmov s nizšimi parami s točki zreniâ ih struktury i klassifikacii. Izdatel'stvo Akademii Nauk SSSR.</ref>.

==== Network Flow-based Decomposition ====

Line 111 ⟶ 108:

The propagation method translates the constraints into a system of equations made up of constants and variables. Then an undirected graph can be built by treating the equations, variables, and constants as nodes and the occurrence of variables and constants in equations as edges. Next, the propagation methods aim at transforming the undirected graph into a directed graph that all equations can be solved in turn. The method begins the computation from the node with constants then tries to propagate the known variable, solutions and constants, to the next node to eliminate the unknown variables.

[https://en.wikipedia.org/wiki/Constraint_programming[Constraint programming|Constraint Programming (CP)]]<ref>Leler, W. (1988). Constraint programming languages: their specification and generation. Addison-Wesley Longman Publishing Co., Inc..</ref> is a standard tool of the propagation method. The numerical CP techniques such as ThingLab<ref>Borning, A. (1981). The programming language aspects of ThingLab, a constraint-oriented simulation laboratory. ACM Transactions on Programming Languages and Systems (TOPLAS), 3(4), 353-387.</ref>, Sketchpad<ref>Sutherland, I. E. (1964). Sketchpad a man-machine graphical communication system. Simulation, 2(5), R-3.</ref>, [https://en.wikipedia.org/wiki/TK_Solver[TK Solver|TK! Solver]] and Juno<ref>Nelson, G. (1985, July). Juno, a constraint-based graphics system. In Proceedings of the 12th annual conference on Computer graphics and interactive techniques (pp. 235-243).</ref> iteratively

approximate the solutions for constraint programs containing cycles. On the other hand, the symbolic methods e.g. Steele's Constraint Language<ref>Steele Jr, G. L. (1980). The definition and implementation of a computer programming language based on constraints.</ref>, Magritte<ref>Gosling, J. A. (1984). Algebraic constraints.</ref>, and IDEAL<ref>Van Wyk, C. J. (1981). A LANGUAGE FOR TYPESETTING GRAPHICS.</ref> are based on algebraic simplification technique. Note that none of the propagation techniques can guarantee to find the solution if there is one. The propagation method is vulnerable for dealing with circularly constrained problems.

Line 126 ⟶ 123:

The algorithms for [[Structural (Combinatorial) Rigidity|structural regidity]] are able to determine the flexibility of the structure formed by rigid bodies and flexible linkages. There are many classic algorithms:

The [https://en.wikipedia.org/wiki/Matroid [matroid]] is used to record the rigidity of rod-and-hinge linkages in any dimensional space. And in two-dimensional space, the classic algorithm [[Laman's Theorem|Laman graphs]] provides a rule to track the internal degree of freedom (DOF) of the system by counting the numbers of edges and vertices.

Some other approaches are proposed to test the bar-joint rigidity for structure in two-dimensional space. For example, network flow-based algorithm<ref>Imai, H. (1985). On combinatorial structures of line drawings of polyhedra. Discrete Applied Mathematics, 10(1), 79-92.</ref>, matroid sums<ref>Gabow, H. N., & Westermann, H. H. (1992). Forests, frames, and games: algorithms for matroid sums and applications. Algorithmica, 7(1-6), 465.</ref>, bipartite matching algorithm<ref>Hendrickson, B. (1992). Conditions for unique graph realizations. SIAM journal on computing, 21(1), 65-84.</ref>, and [[Pebble Game|pebble game]].

Extend to 3-dimensional space, [https://en.wikipedia.org/wiki/[Cauchy%27s_theorem_27s theorem (geometry) |Cauchy’s theorem]] shows that in all [https://en.wikipedia.org/wiki/Convex_polygon[Convex polygon|convex polyhedrons]] are rigid and also globally rigid. And Raoul Bricard and Robert Connelly show that flexible polyhedra which are non-convex polyhedron is not rigid.

<!---

Line 167 ⟶ 160:

{{Reflist}}

--->

<!--- Categories --->

Line 201 ⟶ 191:

article. You don't need to say much, just the key idea and then link to those pages. Currently it seems as though the entire

combinatorial-algebraic part is just tree decomposability and quadratic solvability. They are actually just the basics.

-->

<!-- Instructor 2nd

Please refer to all the relevant articles from my webpage