README

Boollet

Boollet 是一个针对 PHP 的布尔代数工具包。

特性

表达式对象 API
表达式解析器
构建真值表
完整合取/析取范式计算
谢尔盖尔金多项式计算
SAT 和 UNSAT 求解器

要求

PHP >= 8.1

安装

composer require d3lph1/boollet

使用

表达式对象 API

你可以创建一个分别具有一个或两个操作数的 UnaryExpression 或 BinaryExpression

use D3lph1\Boollet\Structure\Expression\{Variable, UnaryExpression, BinaryExpression};
use D3lph1\Boollet\Structure\Operator\{UnaryOperators, BinaryOperators};

$expr = new BinaryExpression(
    new UnaryExpression(UnaryOperators::NOT, new Variable(false)),
    BinaryOperators::AND,
    new BinaryExpression(new Variable(true), BinaryOperators::OR, new Variable(false, label: 'Z'))
);

echo $expr; // (!A ⋀ (B ⋁ Z))

如果没有指定变量的标签，它将被分配为顺序自动生成的符号。

使用初始变量值评估表达式

$val = $expr->evaluate(); // true

使用覆盖的变量值评估表达式（可以是部分覆盖）

$val = $expr->evaluate(['A' => true, 'B' => true, 'Z' => true]) // false

值绑定

在上面的示例中，只有静态变量值，不能在没有表达式重建的情况下动态更改。

要更改运行时变量的值，您应使用 Variable::set() 方法。为了方便批量值设置，有 ValueBinder 类

use D3lph1\Boollet\ValueBinder;

$a = new Variable(false);
$b = new Variable(true);
$z = new Variable(false, label: 'Z');

$expr = new BinaryExpression(
    new UnaryExpression(UnaryOperators::NOT, $a),
    BinaryOperators::AND,
    new BinaryExpression($b, BinaryOperators::OR, $z)
);

$binder = new ValueBinder();
$binder->bind($a);
$binder->bindAll([$b, $z]);

$binder->set([
    'A' => true,
    'B' => true,
    'Z' => true
])

$expr->evaluate(); // true

表达式解析器

对于解析字符串表达式，使用 ShuntingYardParser 解析器实现。底层使用同名的迪杰斯特拉算法。

use D3lph1\Boollet\Parser\{Lexer, Reader\StringInputReader, ShuntingYardParser};

$lexer = Lexer::default();
$input = new StringInputReader('X ⊕ Y → (X ⋀ Z)');
$parser = new ShuntingYardParser($lexer);

$expr = $parser->parse($input);

echo $expr; // ((X ⊕ Y) → (X ⋀ Z))

构建真值表

use D3lph1\Boollet\TruthTable;

$table = TruthTable::tabulate($expr);
$table->setLabel('f(X ⊕ Y → (X ⋀ Z))');

echo $table;

+---+---+---+--------------------+
| X | Y | Z | f(X ⊕ Y → (X ⋀ Z)) |
+---+---+---+--------------------+
| 0 | 0 | 0 |                  1 |
| 0 | 0 | 0 |                  1 |
| 0 | 1 | 0 |                  0 |
| 0 | 1 | 0 |                  0 |
| 1 | 0 | 0 |                  0 |
| 1 | 0 | 0 |                  1 |
| 1 | 1 | 0 |                  1 |
| 1 | 1 | 0 |                  1 |
+---+---+---+--------------------+

完整合取/析取范式计算

类 NormalForms 提供了查找完整合取（或析取）范式表示的实用方法。

use D3lph1\Boollet\NormalForm\NormalForms;

// $expr ~ ((X ⊕ Y) → (X ⋀ Z))

$ccnf = NormalForms::calculateCompleteConjunctive($expr); // ((X ⋁ (!Y ⋁ Z)) ⋀ ((X ⋁ (!Y ⋁ !Z)) ⋀ (!X ⋁ (Y ⋁ Z))))
$cdnf = NormalForms::calculateCompleteDisjunctive($expr); // ((!X ⋀ (!Y ⋀ !Z)) ⋁ ((!X ⋀ (!Y ⋀ Z)) ⋁ ((X ⋀ (!Y ⋀ Z)) ⋁ ((X ⋀ (Y ⋀ !Z)) ⋁ (X ⋀ (Y ⋀ Z))))))

谢尔盖尔金多项式计算

对于此类需求，您可以使用 ZhegalkinPolynomial 实用类

use \D3lph1\Boollet\ZhegalkinPolynomial;

// $expr ~ (!X → ((!Y ⊕ X) ⋀ !Z))

$polynomial = ZhegalkinPolynomial::calculate($expr);

echo $polynomial; // ((Z ⋀ (Y ⋀ X)) ⊕ ((Y ⋀ X) ⊕ ((Z ⋀ X) ⊕ ((Z ⋀ Y) ⊕ (Y ⊕ (Z ⊕ 1))))))

SAT 和 UNSAT 求解器

Boollet 提供了用于解决布尔（不）可满足性问题的简单算法实现。

SAT 是确定是否存在一个解释可以满足给定的布尔公式的（公式变为 true）问题。

UNSAT 是确定是否存在一个解释不能满足给定的布尔公式的（公式变为 false）问题。

CompleteDisjunctiveNormalFormSATSolver 只与完整析取范式表达式一起工作。而 CompleteConjunctiveNormalFormUNSATSolver 只使用完整合取范式表达式。

方法 findAllPossibleSolutions() 的第二个参数接受一个数组，其中包含需要解决该问题的变量。未传递到该参数的标签的其他变量必须有值（在下面的示例中 y 是这样的变量）。

use \D3lph1\Boollet\SAT\CompleteDisjunctiveNormalFormSATSolver;
// $expr ~ X ⋁ (Y ⋀ Z)

$y->set(false);

$cdnf = NormalForms::calculateCompleteDisjunctive($expr);

$sat = new CompleteDisjunctiveNormalFormSATSolver();
$solutions = $sat->findAllPossibleSolutions($cdnf, ['X', 'Z']);
$solutions = $sat->findAllPossibleSolutions($cdnf, ['X', 'Z']);

$solutions 将如下所示

^ array:2 [▼
  0 => array:2 [▼
    "X" => true
    "Z" => false
  ]
  1 => array:2 [▼
    "X" => true
    "Z" => true
  ]
]

要方便地定义结果约束，可以使用 findAllPossibleSolutionsWithConstraints()

use D3lph1\Boollet\Constraints\Constraints;

$solutions = $sat->findAllPossibleSolutionsWithConstraints($cdnf, ['X', 'Z'], new class() implements Constraints {
    public function isSatisfy(array $values): bool
    {
        return $values['X'];
    }
});