LogicLoss

pysignet.loss.LogicLoss

Bases: BatchHandlerMixin

Wrapper for CompiledExpression that adds loss computation.

LogicLoss delegates evaluation to an underlying CompiledExpression, then applies compiler-aware batch reduction via BatchHandlerMixin, and adds loss-specific functionality (post-processing, reduction).

Methods:

Name	Description
satisfaction	Get soft satisfaction values in [0, 1]
loss	Get loss values for training (lower = better)
log_satisfaction	Get log-space satisfaction for stability
partial	Create partially-bound expression

Properties

free_variables: Set of unbound variable names trainable_parameters: List of trainable nn.Parameters

Parameters:

Name	Type	Description	Default
compiled_expr	CompiledExpression	CompiledExpression from compiler.compile()	required
post_processing	str | Callable[[Tensor], Tensor] | None	Default post-processing mode - 'log', 'linear', or callable. If None, uses the compiler's recommendation.	None

Example

from pysignet import logic_to_loss
logic_loss = logic_to_loss(expr, predicates)
sat = logic_loss.satisfaction(X=x)  # Soft truth values
loss = logic_loss.loss(X=x)         # For training
params = logic_loss.trainable_parameters

free_variables property

Return set of variables that still need to be bound.

Delegates to the underlying CompiledExpression.

Returns:

Type	Description
set[str]	Set of variable names not yet bound

trainable_parameters property

All trainable parameters from model-based predicates.

Delegates to the underlying CompiledExpression.

Returns:

Type	Description
list[Parameter]	List of torch.nn.Parameter objects from all model-based
list[Parameter]	predicates

Example

params = logic_loss.trainable_parameters
optimizer = torch.optim.Adam(params, lr=0.001)

__init__(compiled_expr, post_processing=None)

Initialize LogicLoss.

Parameters:

Name	Type	Description	Default
compiled_expr	CompiledExpression	CompiledExpression to wrap	required
post_processing	str | Callable[[Tensor], Tensor] | None	Default post-processing ('log', 'linear', callable). If None, uses the compiler's recommended mode.	None

__repr__()

Return string representation of LogicLoss.

Returns:

Type	Description
str	Multi-line string showing expression, free variables,
str	and post-processing mode.

log_satisfaction(quantify='forall', **variable_bindings)

Compute log-satisfaction for numerical stability.

For product-based compilers with large batches, computing satisfaction in linear space can underflow to zero. When using product conjunction with forall quantification, this method computes sum(log(p_i)) directly instead of log(product(p_i)), which is mathematically identical but avoids underflow.

Parameters:

Name	Type	Description	Default
quantify	Literal['forall', 'exists', 'none']	Batch quantification mode (same as satisfaction())	'forall'
**variable_bindings	Tensor	Variable bindings as keyword arguments (e.g., X=x_tensor, Y=y_tensor)	{}

Returns:

Type	Description
Tensor	Log-satisfaction tensor in (-inf, 0]:
Tensor	Scalar if quantify='forall' or 'exists'
Tensor	(batch_size,) if quantify='none'

Examples:

log_sat = logic_loss.log_satisfaction(X=x)

loss(quantify='forall', reduction='none', post_processing=None, **variable_bindings)

Compute loss based on logical constraint violation.

Parameters:

Name	Type	Description	Default
quantify	Literal['forall', 'exists', 'none']	Batch quantification mode: - 'forall': Universal quantification -> scalar loss - 'exists': Existential quantification -> scalar loss - 'none': No quantification -> per-batch losses	'forall'
reduction	Literal['mean', 'sum', 'none']	Loss reduction mode (only with quantify='none'): - 'mean': Mean of per-batch losses - 'sum': Sum of per-batch losses - 'none': Return per-batch losses	'none'
post_processing	str | Callable[[Tensor], Tensor] | None	Post-processing mode - 'log', 'linear', callable, or None (uses default from init)	None
**variable_bindings	Tensor	Variable bindings as keyword arguments (e.g., X=x_tensor, Y=y_tensor)	{}

Returns:

Type	Description
Tensor	Loss value (lower = better satisfaction):
Tensor	Scalar if quantify='forall'/'exists', or reduction='mean'/'sum'
Tensor	(batch_size,) if quantify='none' and reduction='none'

Raises:

Type	Description
ValueError	If invalid quantify, reduction, or post_processing
ValueError	If reduction != 'none' with quantify='forall'/'exists'

Examples:

loss = logic_loss.loss(X=x)  # scalar
loss = logic_loss.loss(
    X=x, quantify='none', reduction='mean'
)

partial(**variable_bindings)

Create partially-bound LogicLoss with some variables fixed.

Delegates to the underlying CompiledExpression and wraps the result in a new LogicLoss.

Parameters:

Name	Type	Description	Default
**variable_bindings	Tensor	Variable bindings to fix (e.g., X=x)	{}

Returns:

Type	Description
LogicLoss	New LogicLoss with fewer free variables

Raises:

Type	Description
ValueError	If no bindings provided
ValueError	If variable is already bound
ValueError	If variable doesn't exist in expression

Examples:

partial = logic_loss.partial(X=x)
result = partial(Y=y)

satisfaction(quantify='forall', **variable_bindings)

Compute soft satisfaction of the logical expression.

Parameters:

Name	Type	Description	Default
quantify	Literal['forall', 'exists', 'none']	Batch quantification mode: - 'forall': Universal quantification -> scalar - 'exists': Existential quantification -> scalar - 'none': No quantification -> (batch_size,)	'forall'
**variable_bindings	Tensor	Variable bindings as keyword arguments (e.g., X=x_tensor, Y=y_tensor)	{}

Returns:

Type	Description
Tensor	Satisfaction tensor in [0, 1]:
Tensor	Scalar if quantify='forall' or 'exists'
Tensor	(batch_size,) if quantify='none'

Raises:

Type	Description
ValueError	If quantify is invalid

Examples:

sat = logic_loss.satisfaction(X=x)  # scalar (forall)
sat = logic_loss.satisfaction(X=x, quantify='exists')
sat = logic_loss.satisfaction(X=x, quantify='none')