Download the PHP package d3lph1/boollet without Composer
On this page you can find all versions of the php package d3lph1/boollet. It is possible to download/install these versions without Composer. Possible dependencies are resolved automatically.
Informations about the package boollet
Boollet
Boollet is a boolean algebra toolkit for PHP.
Features
- [x] Expression object API
- [x] Expression parser
- [x] Building truth tables
- [x] Complete conjunctive/disjunctive normal form calculation
- [x] Zhegalkin Polynomial calculation
- [x] SAT and UNSAT solvers
Requirements
- PHP >= 8.1
Installation
Usage
Expression object API
You can create either UnaryExpression
or BinaryExpression
with one or two operands respectively:
If there is no label for variable specified, it will be assigned with sequentially autogenerated symbols.
Evaluate the expression with initial variable values:
Evaluate the expression with overwritten variable values (It can be partially overwritten):
Value binding
In the example above there are only static variable values which could not be changed dynamically without expression reconstructing.
To change value of variable at runtime you should use Variable::set()
method. For convenient batch value setup there is ValueBinder
class:
Expression parser
For parsing stringed expressions uses ShuntingYardParser
parser implementation. Under the hood it uses Dijkstra's algorithm of the same name.
Building truth table
Complete conjunctive/disjunctive normal form calculation
Class NormalForms
provides utility methods to find complete conjunctive (or disjunctive ) normal form representations.
Zhegalkin Polynomial calculation
For such needs you can use ZhegalkinPolynomial
utility class:
SAT and UNSAT solvers
Boollet provides naive algorithm implementations to solve boolean (un)satisfiability problem.
SAT is the problem of determining if there exists an interpretation that satisfies a given boolean formula (formula becomes
true
).UNSAT is the problem of determining if there exists an interpretation that not satisfies a given boolean formula (formula becomes
false
).
CompleteDisjunctiveNormalFormSATSolver
works only with expressions in complete disjunctive normal form. Whereas CompleteConjunctiveNormalFormUNSATSolver
uses only expressions in complete conjunctive normal form.
The second argument of the method findAllPossibleSolutions()
takes an array of variables with respect to which it is required to solve the problem.
Other variables whose labels are not passed to this argument must have values (in the example below y
is such variable).
$solutions
will look like this:
To conveniently define results constraints, you can use findAllPossibleSolutionsWithConstraints()
:
$solutions
will look like this:
License
This code is published under the MIT license. This means you can do almost anything with it, as long as the copyright notice and the accompanying license file is left intact.