CLP(B) — Boolean Constraints

CLP(B) provides constraint logic programming over Booleans, enabling SAT solving, tautology checking, model counting, and combinatorial problems. The implementation follows Markus Triska's design using reduced ordered BDDs (Binary Decision Diagrams).

The implementation lives in clausal/logic/clpb.py.

Note

For CLP(FD) (finite-domain integer constraints) and Dif/2 (disequality), see Constraints.

---

Operator Syntax

Python's bitwise operators express Boolean formulas:

Operator	Meaning
X & Y	AND
X \| Y	OR
X ^ Y	XOR
~X	NOT
BoolEq(X, Y)	Equivalence (iff)
BoolImpl(X, Y)	Implication (X → Y)

Variables in CLP(B) are constrained to values 0 (false) and 1 (true).

---

Builtins

Builtin	Arity	Description
Sat	1	Sat(Expr) — post Boolean constraint; fail if unsatisfiable
Taut	2	Taut(Expr, T) — T=1 if tautology, T=0 if contradiction, else fail
SatCount	2	SatCount(Expr, N) — N is the number of satisfying assignments
BoolLabeling	1	BoolLabeling(Vars) — enumerate 0/1 assignments

Sat/1

Posts a Boolean constraint. Fails immediately if the formula is unsatisfiable:

# skip
Sat(X & Y)                # both must be 1
Sat(X | Y)                # at least one must be 1
Sat(~X)                     # X must be 0
Sat(BoolEq(X, Y))         # X ↔ Y (equivalence)
Sat(BoolImpl(X, Y))       # X → Y (implication)

Multiple Sat calls on shared variables build a single constraint network:

# skip
Sat(X | Y), Sat(~X | Z), Sat(Y & Z)

Taut/2

Tests if a formula is a tautology, contradiction, or neither:

# skip
# De Morgan's law — tautology
Taut(BoolEq(~(X & Y), ~X | ~Y), T)   # T = 1

# Contradiction
Taut(X & ~X, T)                          # T = 0

# Neither (indeterminate) — Taut fails
Taut(X | Y, T)                            # fails

SatCount/2

Counts the number of satisfying assignments:

# skip
SatCount(X ^ Y, N)       # N = 2  (XOR has 2 solutions)
SatCount(X & Y, N)       # N = 1  (AND has 1 solution)
SatCount(X | Y, N)       # N = 3  (OR has 3 solutions)

BoolLabeling/1

Enumerates all 0/1 assignments for a list of variables:

solve(X, Y) <- (
    Sat(X ^ Y),
    BoolLabeling([X, Y])
)
# yields (0, 1) and (1, 0)

---

Examples

Half Adder

```clausal

skip

HalfAdder(X, Y, SUM, CARRY) <- (
    Sat(BoolEq(SUM, X ^ Y)),
    Sat(BoolEq(CARRY, X & Y))
)
```

### Pigeon-Hole (unsatisfiable)

3 pigeons in 2 holes — no solution exists:

```clausal

skip

PigeonHole() <- (
    Sat(P11 | P12),
    Sat(P21 | P22),
    Sat(P31 | P32),
    Sat(~(P11 & P21)),
    Sat(~(P11 & P31)),
    Sat(~(P21 & P31)),
    Sat(~(P12 & P22)),
    Sat(~(P12 & P32)),
    Sat(~(P22 & P32)),
    BoolLabeling([P11, P12, P21, P22, P31, P32])
)
# no solutions
```

### Circuit Equivalence

Verify De Morgan's law via tautology check:

```clausal

skip

Taut(BoolEq(~(X & Y), ~X | ~Y), T)   # T = 1
```

---

BDD Internals

CLP(B) uses reduced ordered Binary Decision Diagrams:

• Terminal nodes: BDD_TRUE = 1, BDD_FALSE = 0
• Internal nodes: BDDNode(var_id, high, low) — high is the child when var=1, low when var=0
• Per-variable unique tables: each variable stores its own node lookup dict (Triska/Knuth technique)
• Reduction rule: if high == low, the node is skipped
• Variable ordering: static first-appearance order (no dynamic reordering)

BoolState

Each constrained variable stores a BoolState as an attributed-variable attribute under the key "clpb":

• sat_expr — original Boolean formula (for rebuild on aliasing)
• bdd — current BDD
• root_var — shared root variable linking all vars in the constraint network

Trail safety: every state change creates a new BoolState via put_attr, automatically restored on backtrack.

Connected-Component Merging

When Sat() is called with variables that already have constraints, all connected BDDs are conjoined. This ensures multiple Sat calls sharing variables form a single constraint network.

---

Python API

from clausal.logic.variables import Var, Trail, deref, unify
from clausal.logic.clpb import sat, taut, sat_count, bool_labeling, BoolEq
from clausal.pythonic_ast.nodes import BitAnd, BitOr, BitXor, Invert

trail = Trail()
x, y = Var(), Var()

# Post constraint: X XOR Y
sat(BitXor(left=x, right=y), trail)

# Enumerate solutions
for _ in bool_labeling([x, y], trail):
    print(deref(x), deref(y))   # 0 1, then 1 0

# Tautology check
t = Var()
taut(BitOr(left=x, right=Invert(operand=x)), t, Trail())
# t = 1

# Model counting
n = Var()
sat_count(BitXor(left=Var(), right=Var()), n, Trail())
# n = 2

---

Interaction with Other Constraints

CLP(B) uses attribute key "clpb", independent of CLP(FD) ("fd"), CLP(R) ("real"), and dif/2 ("dif"). All hooks fire independently when a variable is bound.

CLP(B) variables are constrained to 0/1 (integers), not Python booleans (True/False). Booleans are explicitly rejected by CLP(R) and CLP(FD) — they are distinct types in Clausal's constraint system. If you need to bridge CLP(B) with numeric constraints, bind via 0/1.

---

Test coverage

Tests are in tests/test_clpb.py (87 tests).

• BDD operations: make_node, apply, restrict, _expr_to_bdd
• Sat: forcing, contradiction, tautology, sequential conjunction
• Taut: tautology/contradiction/indeterminate
• SatCount: various formulas
• BoolLabeling: unconstrained, constrained
• Attribute hook: bind, merge, incompatible
• Trail safety: backtrack, labeling
• Half adder: complete truth table
• Full adder: 5 input combinations
• Pigeon-hole: unsatisfiable
• Circuit equivalence: De Morgan's law