有什么方法可以在SymPy中获得逐步解决方案吗？

Question

有什么方法可以在SymPy中获得逐步解决方案吗？例如：

x**2-5 = 4
  step 1 x**2-5+5=4+5
  step 2 : x**2=9
  step 3 :x = 3 or x= -3

Answer 1

（这更多的是作为答案的评论）

有一些 Google 的 soc 想法可供实施

逐步表达可视化

GSoC 2014 想法： 很多时候，人们会问如何知道某些函数正在做什么。比如，他们想一步步了解……对于前者，你最好就是按照代码来；对于后者，算法根本不像你手工做的那样工作，所以真的没有办法......

GSoC 2015 想法：

循序渐进的策略

许多 SymPy 操作背后的逻辑被分成几个小方法。例如，像 sin 或 exp 这样的对象具有 _eval_derivative 方法，这些方法被称为 SymPy 计算像 sin(exp(x)) 这样的复杂表达式的导数。通过捕获所有这些小方法的输入和输出，我们可以收集有关 SymPy 所采取步骤的大量信息。我们可以看到 exp._eval_derivative 接受 exp(x) 并返回 exp(x)，而 sin._eval_derivative 接受 sin(exp(x)) 并返回 cos(exp(x))*exp(x)。每种方法的这些输入输出对可能足以说明 SymPy 如何解决许多领域的问题。

这种捕获许多内部函数输入的方法类似于传统上用于分析大型代码库的日志系统。我们应该调查它们是如何工作的以及它们是否对正常操作造成任何问题。

一旦获得了该信息源，我们就可以考虑有趣的方式来可视化并与之交互。一个好的解决方案不会将数据流与特定的可视化技术不可撤销地联系在一起。

这种方法在智力上很简单，但可能需要学生与大量代码库进行交互。像 _eval_derivative 这样的方法在 SymPy 中无处不在，但在不同的模块中通常有微小的变化。

这里有一个在线解决方案SymPy Gamma

Answer 2

简单情况的临时解决方案可能基于表达式树。一开始，您可以创建一个不进行求值的表达式树。之后您可以逐级修改结果：

源代码：

class TraverseSolver:
    def __init__(self, expr):
        self.expr = expr
        
    def _set_graph(self):
        self.G = nx.nx_agraph.from_agraph(pygraphviz.AGraph(sp.dotprint(self.expr))) 
        
    def _set_map(self):
        self._map = dict(zip(self.G.nodes, sp.preorder_traversal(self.expr))) 
        
    def _set_baseNode(self):
        self._baseNode = next(iter(self.G.nodes))
        
    def get_levels(self, mode='draw'):
        if mode == 'draw':
            d = nx.single_source_shortest_path_length(self.G, self._baseNode)
            u, idx = np.unique(list(d.values()), return_index=True)
            levels = [[str(m) for m in n] for n in reversed(np.split(np.array(list(d.keys())), idx[1:]))]
            return levels
        elif mode == 'traverse':
            print(self.G)
    
    def set_color(self, node, color):
        self.G.nodes[node]['color'] = color

    def display_graph(self, fig, n, nshape=(2, 3)):      
        ax = fig.add_subplot(*nshape, n)
        pos = graphviz_layout(self.G, prog='dot')
        colors = nx.get_node_attributes(self.G, 'color')    
        nx.draw(self.G, pos = pos, nodelist=[])
        # draw self.G bbox by bbox:
        for i, n in enumerate(self.G.nodes()):
            nx.draw(nx.subgraph(self.G, [n]), pos={n:pos[n]}, labels = {n:f'${sp.latex(self._map[n])}$'}, nodelist=[],
                    bbox=dict(facecolor=colors[n], edgecolor='black', boxstyle='round,pad=0.7'))
            
    def solve(self, display_graph=True, nshape=(2, 3)):
        self._set_graph() #store sp.srepr+code in each node
        self._set_map() #sp.srepr+code -> expression (without evaluation)
        self._set_baseNode() #sp.srepr+code of self.
        solutionSteps = [self._map[self._baseNode]] #first step that contains initial expression
        levels = self.get_levels(mode='draw')
        if display_graph:
            fig = plt.figure(figsize=(20,10))
        #Step forward
        for i in range(len(levels)):
            if display_graph:
                for node in self.G.nodes(): 
                    self.set_color(node, 'lightblue')
            anyChanges = False
            for activeNode in levels[i]:
                beforeEval = self._map[activeNode]
                if display_graph:
                    self.set_color(activeNode, 'yellow')
                if not beforeEval.is_Atom:
                    afterEval = beforeEval.func(*beforeEval.args, evaluate=True) #is beforeEval different with afterEval
                    if beforeEval != afterEval:
                        self._map[activeNode] = afterEval
                        if display_graph:
                            self.set_color(activeNode, 'lime')
                        anyChanges = True
            # Calculate value of baseNode() using changes, no evaluation      
            if anyChanges:
                for j in range(i+1, len(levels)):
                    for editNode in levels[j]:
                        args = [self._map[node] for node in self.G[editNode]] #each ancestor
                        if not self._map[editNode].is_Atom:
                            self._map[editNode] = self._map[editNode].func(*args, evaluate=False)
                solutionSteps.append(self._map[self._baseNode])
            if display_graph:
                self.display_graph(fig, n=len(solutionSteps), nshape=nshape)
        plt.show()
        return solutionSteps

expr = sp.sympify('-1*(2*3-5*7)', evaluate=False)
steps = TraverseSolver(expr).solve(display_graph=True, nshape=(2, 3))

print('INPUT:', sp.srepr(expr))
print('SOLUTION 1:', ' = '. join([str(step) for step in steps]))
print('SOLUTION 2:', ' = '. join([sp.StrPrinter(dict(order='none'))._print(step) for step in steps])) 

输出：

INPUT: Mul(Integer(-1), Add(Mul(Integer(-1), Mul(Integer(5), Integer(7))), Mul(Integer(2), Integer(3))))
SOLUTION 1: -(-5*7 + 2*3) = -(-1*35 + 2*3) = -(-35 + 6) = -1*(-29) = 29
SOLUTION 2: -(2*3 - 5*7) = -(2*3 - 1*35) = -(6 - 35) = -1*(-29) = 29

要求：

networkx

、

matplotlib

、

python-graphviz

Answer 3

关于graphviz的答案，这里是对源代码的更正。另请注意，python-graphviz 是 pip 中的 pygraphviz：

import networkx as nx
import matplotlib
import pygraphviz
import sympy as sp
import numpy as np
from matplotlib import pyplot as plt


class TraverseSolver:
    def __init__(self, expr):
        self.expr = expr

    def _set_graph(self):
        self.G = nx.nx_agraph.from_agraph(pygraphviz.AGraph(sp.dotprint(self.expr)))

    def _set_map(self):
        self._map = dict(zip(self.G.nodes, sp.preorder_traversal(self.expr)))

    def _set_baseNode(self):
        self._baseNode = next(iter(self.G.nodes))

    def get_levels(self, mode='draw'):
        if mode == 'draw':
            d = nx.single_source_shortest_path_length(self.G, self._baseNode)
            u, idx = np.unique(list(d.values()), return_index=True)
            levels = [[str(m) for m in n] for n in reversed(np.split(np.array(list(d.keys())), idx[1:]))]
            return levels
        elif mode == 'traverse':
            print(self.G)

    def set_color(self, node, color):
        self.G.nodes[node]['color'] = color

    def display_graph(self, fig, n, nshape=(2, 3)):
        ax = fig.add_subplot(*nshape, n)
        pos = nx.nx_pydot.graphviz_layout(self.G, prog='dot')
        colors = nx.get_node_attributes(self.G, 'color')
        nx.draw(self.G, pos = pos, nodelist=[])
        # draw self.G bbox by bbox:
        for i, n in enumerate(self.G.nodes()):
            nx.draw(nx.subgraph(self.G, [n]), pos={n:pos[n]}, labels = {n:f'${sp.latex(self._map[n])}$'}, nodelist=[],
                    bbox=dict(facecolor=colors[n], edgecolor='black', boxstyle='round,pad=0.7'))

    def solve(self, display_graph=True, nshape=(2, 3)):
        self._set_graph() #store sp.srepr+code in each node
        self._set_map() #sp.srepr+code -> expression (without evaluation)
        self._set_baseNode() #sp.srepr+code of self.
        solutionSteps = [self._map[self._baseNode]] #first step that contains initial expression
        levels = self.get_levels(mode='draw')
        if display_graph:
            fig = plt.figure(figsize=(20,10))
        #Step forward
        for i in range(len(levels)):
            if display_graph:
                for node in self.G.nodes():
                    self.set_color(node, 'lightblue')
            anyChanges = False
            for activeNode in levels[i]:
                beforeEval = self._map[activeNode]
                if display_graph:
                    self.set_color(activeNode, 'yellow')
                if not beforeEval.is_Atom:
                    afterEval = beforeEval.func(*beforeEval.args, evaluate=True) #is beforeEval different with afterEval
                    if beforeEval != afterEval:
                        self._map[activeNode] = afterEval
                        if display_graph:
                            self.set_color(activeNode, 'lime')
                        anyChanges = True
            # Calculate value of baseNode() using changes, no evaluation
            if anyChanges:
                for j in range(i+1, len(levels)):
                    for editNode in levels[j]:
                        args = [self._map[node] for node in self.G[editNode]] #each ancestor
                        if not self._map[editNode].is_Atom:
                            self._map[editNode] = self._map[editNode].func(*args, evaluate=False)
                solutionSteps.append(self._map[self._baseNode])
            if display_graph:
                self.display_graph(fig, n=len(solutionSteps), nshape=nshape)
        plt.show()
        return solutionSteps

expr = sp.simplify('-1*(2*3-5*7)', evaluate=False)
steps = TraverseSolver(expr).solve(display_graph=True, nshape=(2, 3))

print('INPUT:', sp.srepr(expr))
print('SOLUTION 1:', ' = '. join([str(step) for step in steps]))
print('SOLUTION 2:', ' = '. join([sp.StrPrinter(dict(order='none'))._print(step) for step in steps]))

Answer 4

这个想法是成对地组合表达式并迭代地建立知识库。您将得到一棵包含所有可能组合的树。

现在您可以采用这棵树，从解决方案节点开始，一直到树的根。这样您就可以跟踪获得解决方案的沿袭（步骤）。

def prove_by_contradiction(premises, hypothesis):
    # Initialize knowledge base and lineage tracking
    knowledge_base = set(premises)
    lineage = {expr: ("knowledge base",) for expr in premises}

    # Step 1: Negate the hypothesis and add it to the knowledge base
    neg_hypothesis = Not(hypothesis)
    knowledge_base.add(neg_hypothesis)
    lineage[neg_hypothesis] = ("negated hypothesis",)

    # Start the proof process
    while True:
        new_knowledge_base = knowledge_base.copy()

        # Step 3: Pairwise combine knowledge base items using simplify_logic
        for expr1, expr2, combined_expr in combine_expressions(knowledge_base):
            # Check for contradiction (sympy's S.false)
            if combined_expr is S.false:
                # Trace back the lineage to the root
                return trace_lineage(lineage, expr1, expr2, combined_expr)

            if combined_expr not in new_knowledge_base:
                new_knowledge_base.add(combined_expr)
                lineage[combined_expr] = (expr1, expr2)

        # Update knowledge base if new expressions have been added
        if new_knowledge_base == knowledge_base:
            break  # Exit if no new knowledge is generated
        knowledge_base = new_knowledge_base

    return "No contradiction found, proof incomplete."

完整要点可以在这里

找到