Conjuctive-Normal-Form builder
import { CNFBuilder } from "cnf-builder";
const builder = new CNFBuilder();
const Alice = builder.addVariable("Alice");
const Bob = builder.addVariable("Bob");
builder.addComments("My first cnf.");
builder.addClause(CNFClause.and([Alice, Bob.not]));
console.log(builder.build());
// c My first cnf.
// p cnf 2 2
// 1 0
// -2 0Always true.
Always false.
A ∧ B ∧ C ...
A ∨ B ∨ C ...
¬A ∧ ¬B ∧ ¬C ...
P ⇒ Q
P ⇔ Q
A ⇔ B ⇔ C ...
There are at most one true variable.
There are at least one true variables.
There are exactly one true variable.