程序可通过直接点击 项目地址 打开（推荐使用 Firefox。对于 Chrome 无法使用模块高亮），
之后在“解析文本”按钮上面的文本框内输入“逆波兰逻辑表达式”，
“逆波兰逻辑表达式”支持五种逻辑操作符：
{
“.”：“a b .”代表“a”和“b”的逻辑与，
“,”：“a b ,”代表“a”和“b”的逻辑或，
“<”：“a <”代表“a”的逻辑非，
“>”：“a b >”代表“a”和“b”的逻辑推出，
“=”：“a b =”代表“a”和“b”的逻辑等价/同或
}，
逆波兰逻辑表达式组合的举例说明：
{
“a b . fe >”即代表逻辑表达“a 与 b 推出了 fe”，
“a b . fe ge > =”即代表逻辑表达“a 与 b 等价于 fe 推出了 ge”
}，
之后点击“解析文本”按钮，将“逆波兰逻辑表达式”转换为适合图形表示的 JSON 格式，
之后再点击“解析文本”按钮旁的“文本转图”，得到最终的正规图形表示。
对于想了解其原理的同学，本目录下的 SATSolver.pdf 是其预印版（preprint）论文。