Draft:Geometric constraint solving
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 (false negative). However, it is not allowed to provide a solution that does not exist (false positive).
Given a geometric constraint system (GCS) with 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 genericity of a GCS is important to know before finding the solutions. Whether a system is generic determines which type of solvers we can use. It is called generic when each of the variables in a system has approximate degree-of-freedom and each constraint corresponds to at least one equation.[3] The property of a generic system is well-behaved that we can use both combinatorial and 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 non-generic if it has these nonideal properties. Only algebraic methods are able to solve non-generic systems since they are not structural (combinatorial).
Given a graph with constraints , 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?
- No, it does not have a solution (over-constrained).
Generic system → How to remove dependent constraints edges to make an over-constrained graph well-constrained?[4] (See rigidity method)
Non-generic system → How to remove dependent equations to make all equations in the system independent?
- Yes, it has a finite number set of solutions (well-constrained).
Generic system → Use combinatorial approaches to solve the realizations (algebraic-based methods also worked but lack of efficiency).
Non-generic system → Use algebraic algorithm to solve the realizations.
- Yes, it has an infinite number set of solutions (under-constrained).
Generic system → Add more constraint edges to make the graph rigid.
Non-generic system → Use configuration space[5] to describe the solution space.
The geometric constraint solvers can be classified into three categories: 1) algebraic & automated geometry theorem proving methods; 2) combinatorial-algebraic algorithm and 3) combinatorial algorithm. The algebraic-based solvers treat GCS as a system of polynomial equations and solve it algebraically in either synthetic or algebraic form. The combinatorial algorithm leverages geometric properties of structure such as 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[6]
Solving a geometric constraint problem is equivalent to 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. 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 mathematic education CAD, robotic, computer vision, and artificial intelligence.
automated geometry theorem proving can be classified into three types based on the different foundations: algebraic, synthetic, semi-synthetic, and numerical.
Synthetic Form
synthetic method does not use coordinates and algebraic formula for representing geometric statements. Instead, it proves theorems by leveraging geometric properties e.g. triangle inequality and 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 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[7] is one of the first automated reasoning systems. After that, the researchers proposed GRAMY[8] and iGeoTutor[9] based on the deductive database method. Moreover, the logic-based methods are also developed to prove the geometrics theorems such as ArgoCLP[10] and OTTER[11]
Semi-synthetic Form
The semi-synthetic method combines synthetic and algebraic methods to obtain the merits of human-readability and computational efficiency. The semi-synthetic method does not use algebra to express geometry problems directly. Instead, it uses geometric quantities to represent conjectures. Then, prove the conjectures by manipulating the equalities in their geometric quantities. As a result, sometimes people also call the semi-synthetic method as coordinate-free methods. Similar to the pure synthetic method, semi-synthetic can also face combinatorial explosion but in most of cases it can produce readable proofs. This approach can be categorized into four types based on the geometric properties they used: area, full-angle, vector, and mass-point methods.
Area Methods
The area method uses geometric quantities to prove many more complex theorems such as Varignon’s theorem and Pascal's theorem.
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 Simson’s theorem, Miquel's theorem, and Five circle theorem.
Vector-based Methods[12]
As the name implies, vector-based method use geometry quantities related to vectors for the proof such as the linearity property of the inner product. Some more complex theorem such as the Orthocenter theorem and Cantor's Theorem can be proved by vector-based methods.
Mass-Point Methods
The mass-point method directly utilizes geometric points instead of geometric quantities. The properties of the barycentric point are used as the proposition for the proofs. Many geometric statements can be proved by mass-point methods including Pappus' theorem and Butterfly Theorem for quadrilaterals.
Algebraic Form
The algebraic method translates the representation of geometric statements into a 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 numerical method translates geometric constraints into algebraic linear or non-linear equations. Then using numerical methods such as Newton-Raphson, Lagrange interpolation polynomial, and Gaussian elimination to approach the solution.
Symbolic Methods
The symbolic methods such as Buchberger and Wu-Ritt are able to compute the 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 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 Buchberger's Algorithm to formulate polynomial equations that can record the addition and deletion of constraints.
Coordinate-Free Method
The coordinate-free methods are the solvers for 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[13] and 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 undirected graph sitting on top of a framework, where the nodes represent the geometric elements and the edges denote the constraints. When the numbers of geometric elements and constraints 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 (DR-planning) and propagation method.
Decomposition Recombination Planning
The decomposition recombination planning (DR-planning) method designs a plan for decomposing a constraint system into multiple smaller subsystems then recombining solutions of these subsystems. DR-planning is efficient but can not be applied to any arbitrary graph-based problems e.g. non-generic system. The solutions of small subsystems must be able to recombine into a global solution of the entire system. Specifically, it is required to substitute the solutions of subsystems to the larger problems and eliminate its variables. By hierarchically substituting solutions of smaller subsystems to larger ones, the entire system can be easy to solve in the end[14][15][16][17][18].
Decomposition
Ruler and Compass
Ruler and compass is a constructive method leveraging the fact that the most complex configuration in engineering drawings can be solved by using small tools like a ruler and compass. This method only considers the graph comprises of points, lines, circles and arcs of a circle. The ruler and compass method has an analyzer and a constructor. The analyzer determines whether the given constraint-graph is solvable by generating a sequence of constructive steps to test if the constraints hold. The constructor in charge of numerical computation, which uses the construction steps to produce geometric elements for the current dimension values.
Triangle (Tree) Decomposition
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[19] is the pioneer of the top-down method which decomposes the constraint graph into smaller 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 rigidity of framework. This type of DR-planning algorithm performs maximum matching on bipartite graphs to generate the DR-plan. Such algorithms include Dulmage-Mendelsohn Decomposition and Assur Decomposition[20].
Network Flow-based Decomposition
The bottom-up DR-planning methods use network flow techniques to solve the GCS problems.[21] The bottom-up method guarantees that the output of the DR-plan has cluster minimality where no sibset of children union is dense. The approaches in this category including frontier vertex decomposition[22] and canonical decomposition.
Optimization of Recombination
After decomposition and obtained the realization for each subsystem, we need to recombine all solutions of each subsystem to get the final solution for the entire system. The algorithm leverages incidence tree parametrizations for a collection of rigid bodies is proposed to minimize the algebraic complexity of the recombination process[23][24][25][26][27].
Propagation Method
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.
Constraint Programming (CP)[28] is a standard tool of the propagation method. The numerical CP techniques such as ThingLab[29], Sketchpad[30], TK! Solver and Juno[31] iteratively approximate the solutions for constraint programs containing cycles. On the other hand, the symbolic methods e.g. Steele's Constraint Language[32], Magritte[33], and IDEAL[34] 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.
Unlike algebraic methods, combinatorial approaches only deal with abstract objects and constraints. These methods determine the properties of the given framework including the analysis of the constraint graphs and degree of freedom (DOF); moreover, categorizing the types of frameworks and determining the rigidity of structures. It is limited to apply combinatorial solvers only on generic GCS since all the theorems and algorithms are using the corresponding graph of the system.
Constraint Graph & Degree of Freedom
Let a geometric constraint graph corresponding to a GCS with weighting and for vertices and edges. These weighting represent the number of DOF available to a with its corresponding object removed by the incident edges. Given a subgraph , we can compute its dense . The dense can be used to determine the constrainedness and degree of freedom of graph.
Types of Framework
Assigning different CGS with a suitable type of framework and solve it is also an important topic in combinatorial approaches. There are various kinds of structure such as bar-joint, Body-and-Cad[37], and Body bar hinge.
Structural Rigidity
The algorithms for structural regidity are able to determine the flexibility of the structure formed by rigid bodies and flexible linkages. There are many classic algorithms:
The 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 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[38], matroid sums[39], bipartite matching algorithm[40], and pebble game.
Extend to 3-dimensional space, Cauchy’s theorem shows that in all 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.
Category:Constraint programming
Category:Articles created via the Article Wizard
- ^ Sitharam, M., John, A. S., & Sidman, J. (2018). Handbook of Geometric Constraint Systems Principles. Chapman and Hall/CRC
- ^ Bouma, W., Fudos, I., Hoffmann, C., Cai, J., & Paige, R. (1995). Geometric constraint solver. Computer-Aided Design, 27(6), 487-501.
- ^ Sitharam, M., & Zhou, Y. (2004). Mixing features and variational constraints in 3d. CAD, available upon request.
- ^ Hoffmann, C., Sitharam, M., & Yuan, B. (2004). Making constraint solvers useable: overconstraints. Comp. Aided Design.
- ^ Sitharam, M., & Gao, H. (2010). Characterizing graphs with convex and connected cayley configuration spaces. Discrete & Computational Geometry, 43(3), 594-625.
- ^ 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.
- ^ 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).
- ^ Matsuda, N., & Vanlehn, K. (2004). Gramy: A geometry theorem prover capable of construction. Journal of Automated Reasoning, 32(1), 3-33.
- ^ Wang, K., & Su, Z. (2015, June). Automated geometry theorem proving for human-readable proofs. In Twenty-Fourth International Joint Conference on Artificial Intelligence.
- ^ 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.
- ^ Beeson, M., & Wos, L. (2014, July). OTTER proofs in Tarskian geometry. In International Joint Conference on Automated Reasoning (pp. 495-510). Springer, Cham.
- ^ 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).
- ^ Sidman, J. & Traves, W. Cayley Factorizationandspecial Positions. In: Sitharaman, M., St.John, A., and Sidman, J. (ed.), Handbook of Geometric Constraints Systems: Principles.
- ^ Baker, T., Sitharam, M., Wang, M., & Willoughby, J. (2015). Optimal decomposition and recombination of isostatic geometric constraint systems for designing layered materials. Computer Aided Geometric Design, 40, 1-25.
- ^ Sitharam, M., & Zhou, Y. (2004). Solving minimal, wellconstrained, 3D geometric constraint systems: combinatorial optimization of algebraic complexity.
- ^ Hoffmann, C. M., Lomonosov, A., & Sitharam, M. (2001). Decomposition of Geometric Constraints Part I: performance measures & Part II: new algorithms. J. of Symbolic Computation, 31(4).
- ^ Hoffman, C. M., Lomonosov, A., & Sitharam, M. (2001). Decomposition plans for geometric constraint problems, part II: new algorithms. Journal of Symbolic Computation, 31(4), 409-427.
- ^ Hoffmann, C. M., Lomonosov, A., & Sitharam, M. (1999, September). Planning Geometric constraint decomposition via optimal graph transformations. In International Workshop on Applications of Graph Transformations with Industrial Relevance (pp. 309-324). Springer, Berlin, Heidelberg.
- ^ 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).
- ^ 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.
- ^ Hoffmann, C. M., Lomonosov, A., & Sitharam, M. (1998). Geometric constraint decomposition. In Geometric constraint solving and applications (pp. 170-195). Springer, Berlin, Heidelberg.
- ^ Oung, J., Sitharam, M., Moro, B., & Arbree, A. (2001, May). FRONTIER: fully enabling geometric constraints for feature-based modeling and assembly. In Proceedings of the sixth ACM symposium on Solid modeling and applications (pp. 307-308).
- ^ Sitharam, M., Zhou, Y., & Peters, J. (2010). Reconciling conflicting combinatorial preprocessors for geometric constraint systems. International Journal of Computational Geometry & Applications, 20(06), 631-651.
- ^ Sitharam, M., Peters, J., & Zhou, Y. (2004). Solving minimal, wellconstrained, 3d geometric constraint systems: combinatorial optimization of algebraic complexity. Automated deduction in Geometry (ADG).
- ^ Sitharam, M. (2006). Well-formed systems of point incidences for resolving collections of rigid bodies. International Journal of Computational Geometry & Applications, 16(05n06), 591-615.
- ^ Sitharam, M., Arbree, A., Zhou, Y., & Kohareswaran, N. (2006). Solution space navigation for geometric constraint systems. ACM Transactions on Graphics (TOG), 25(2), 194-213.
- ^ Peters, J., Sitharam, M., Zhou, Y., & Fan, J. (2006). Elimination in generically rigid 3d geometric constraint systems. In Algebraic Geometry and Geometric Modeling (pp. 205-216). Springer, Berlin, Heidelberg.
- ^ Leler, W. (1988). Constraint programming languages: their specification and generation. Addison-Wesley Longman Publishing Co., Inc..
- ^ 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.
- ^ Sutherland, I. E. (1964). Sketchpad a man-machine graphical communication system. Simulation, 2(5), R-3.
- ^ 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).
- ^ Steele Jr, G. L. (1980). The definition and implementation of a computer programming language based on constraints.
- ^ Gosling, J. A. (1984). Algebraic constraints.
- ^ Van Wyk, C. J. (1981). A LANGUAGE FOR TYPESETTING GRAPHICS.
- ^ Sitharam, M. (2005). Combinatorial approaches to geometric constraint solving: Problems, progress, and directions. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 67, 117.
- ^ Wang, M., & Sitharam, M. (2014, July). Combinatorial rigidity and independence of generalized pinned subspace-incidence constraint systems. In International Workshop on Automated Deduction in Geometry (pp. 166-180). Springer, Cham.
- ^ Haller, K., John, A. L. S., Sitharam, M., Streinu, I., & White, N. (2012). Body-and-cad geometric constraint systems. Computational Geometry, 45(8), 385-405.
- ^ Imai, H. (1985). On combinatorial structures of line drawings of polyhedra. Discrete Applied Mathematics, 10(1), 79-92.
- ^ Gabow, H. N., & Westermann, H. H. (1992). Forests, frames, and games: algorithms for matroid sums and applications. Algorithmica, 7(1-6), 465.
- ^ Hendrickson, B. (1992). Conditions for unique graph realizations. SIAM journal on computing, 21(1), 65-84.