Binary perceptron and random K-SAT
A binary perceptron that must store random patterns, revealed one per step, as cardinality constraints.
- Name:
perceptron_satisfiability - Field:
computer_science/neural_networks - Formalism: agent-based model
- References: Bertin 2021; Krauth and Mezard 1989
Factory
@register_model(
field='computer_science/neural_networks',
tags=('perceptron', 'satisfiability', 'disorder', 'critical load'),
references=('Bertin 2021', 'Krauth and Mezard 1989'),
defaults={'until': 31},
)
def perceptron_satisfiability(
n_weights: int = 21,
*,
load: float = 1.5,
random_state: int | np.random.Generator | None = 0,
) -> System:
"""Return a binary perceptron that must store random patterns, revealed one per step, as cardinality constraints.
A pattern `xi` of output `sigma` holds when `sigma sum_i w_i xi_i > 0`, so with an odd number `N` of weights
`w_i = +-1`, when at least `(N + 1) / 2` of the literals `w_i = sigma xi_i` hold. The patterns are satisfiable up to
the critical load `p / N` of about 0.83 in the limit of many weights (Bertin 2021 §6.3.3, Ex. 6.4). The patterns are
drawn from `random_state`, so a disorder average sweeps it through `GridDesign`.
Args:
n_weights:
The number of weights, which is odd.
load:
The number of patterns over the number of weights.
random_state:
The seed or generator of the patterns.
Returns:
system:
The model, with the group `weights` and the reports `decide.satisfiable` and `decide.revealed`.
Raises:
ValidationError:
The number of weights is even, so a pattern can tie.
Examples:
>>> from skcomplex.models.computer_science.neural_networks import perceptron_satisfiability
>>> perceptron_satisfiability(3, load=1.0).interactions[0].constraints[0].bound
2
"""
if n_weights % 2 == 0:
error_msg = f'perceptron_satisfiability has n_weights={n_weights!r}. Use an odd number, so no pattern ties.'
raise ValidationError(error_msg)
rng = np.random.default_rng(random_state)
n_patterns = round(load * n_weights)
patterns = rng.choice([-1, 1], size=(n_patterns, n_weights)) * rng.choice([-1, 1], size=(n_patterns, 1))
indices = np.arange(1, n_weights + 1)
constraints = [
CardinalitySpec(tuple((indices * pattern).tolist()), (n_weights + 1) // 2, 'at-least') for pattern in patterns
]
weights = GroupElement('weights', element=BinaryWeightElement, size=n_weights)
decide = SatisfiabilityInteraction('decide', target='weights', state='on', constraints=constraints)
return System(elements=[weights], interactions=[decide], time=DiscreteTime())
Components
class BinaryWeightElement(Element):
"""Weight of a binary perceptron, where the state 1 stands for `+1` and the state 0 for `-1`.
Args:
label:
The label of the weight or the group.
on:
Whether the weight is `+1`.
Examples:
>>> from skcomplex.models.computer_science.neural_networks import BinaryWeightElement
>>> BinaryWeightElement('weight', on=1.0).on
1.0
"""
def __init__(self, label: str, on: Annotated[float, StateSpec(domain=FiniteEnumeratedSet([0, 1]))] = 0.0) -> None:
super().__init__(label)
self.on = on
class SatisfiabilityInteraction(Interaction):
"""Reveal constraints on the Boolean states of a group step by step, and decide them with one incremental solver.
Every step adds the next `reveal` constraints to one PySAT solver, which keeps what it learned, and sets the states
of the members to a satisfying assignment when one exists. The interaction reports `satisfiable`, 1 or 0, and
`revealed`, the number of active constraints, every step. A state that is not Boolean is reported by the compiler
with the code `law-domain`.
Args:
label:
The label of the interaction.
target:
The path of the group.
state:
The name of the Boolean state of the members.
constraints:
The constraints, in the order they are revealed.
reveal:
The number of constraints revealed per step.
solver:
The name of the PySAT solver.
phase:
The name of the phase of the step the rule runs in, or `None` for the default phase.
Raises:
ValidationError:
A constraint is not a spec or the number revealed per step is not positive, raised by `check`.
Examples:
>>> from skcomplex.core.interactions import SatisfiabilityInteraction
>>> from skcomplex.specs import ClauseSpec
>>> interaction = SatisfiabilityInteraction('sat', target='bits', state='on', constraints=[ClauseSpec((1, -2))])
>>> interaction.check().reveal
1
"""
reports: ClassVar[tuple[str, ...]] = ('satisfiable', 'revealed')
def __init__(
self,
label: str,
*,
target: Annotated[str, RoleSpec()],
state: str,
constraints: Sequence[ClauseSpec | CardinalitySpec],
reveal: int = 1,
solver: str = 'cadical153',
phase: str | None = None,
) -> None:
super().__init__(label)
self.target = target
self.state = state
self.constraints = constraints
self.reveal = reveal
self.solver = solver
self.phase = phase
def _check(self) -> None:
"""Raise an error for a constraint that is not a spec, or a number revealed per step that is not positive.
Raises:
ValidationError:
A constraint is not a spec or the number revealed per step is not positive.
"""
super()._check()
if self.reveal < 1:
error_msg = f'The satisfiability {self.label!r} has reveal={self.reveal!r}. Reveal at least 1 per step.'
raise ValidationError(error_msg)
for constraint in self.constraints:
if not isinstance(constraint, ClauseSpec | CardinalitySpec):
error_msg = f'The constraint {constraint!r} of {self.label!r} is no ClauseSpec or CardinalitySpec.'
raise ValidationError(error_msg)
constraint.check()
def _add(self, constraint: ClauseSpec | CardinalitySpec, solver: Solver, pool: IDPool) -> None:
"""Add one constraint to the solver, encoding a cardinality constraint with variables of the shared pool."""
if isinstance(constraint, ClauseSpec):
solver.add_clause(list(constraint.literals))
return
encode = CardEnc.atleast if constraint.sense == 'at-least' else CardEnc.atmost
for clause in encode(lits=list(constraint.literals), bound=constraint.bound, vpool=pool).clauses:
solver.add_clause(clause)
def _decide(self, model: ModelViewProtocol) -> None:
"""Reveal the next constraints, decide them, and set the members to a satisfying assignment when one exists."""
agents = model.agents(self._get_role('target'))
if 'solver' not in model.storage:
model.storage.update(
solver=Solver(name=self.solver),
pool=IDPool(start_from=len(agents) + 1),
revealed=0,
)
solver = cast(Solver, model.storage['solver'])
pool = cast(IDPool, model.storage['pool'])
revealed = cast(int, model.storage['revealed'])
following = min(revealed + self.reveal, len(self.constraints))
for constraint in self.constraints[revealed:following]:
self._add(constraint, solver, pool)
model.storage['revealed'] = following
satisfiable = solver.solve()
if satisfiable:
holding = {literal for literal in solver.get_model() if literal > 0}
for index, agent in enumerate(agents, start=1):
setattr(agent, self.state, float(index in holding))
model.report('satisfiable', float(satisfiable))
model.report('revealed', float(following))
def _get_laws(self, namespace: SimpleNamespace) -> list[BaseLaw]:
"""Return the rule of one step.
Args:
namespace:
The namespace of the symbols the laws can use, which the rule does not read.
Returns:
laws:
The rule that reveals and decides constraints.
"""
return [RuleLaw(self._decide, phase=self.phase)]