This website uses Javascript to render markdown documents in your browser, apply syntax highlighting to code fragments and render $\LaTeX$ formulas. Below is the markdown source code of this page. You can either read that or enable Javascript to have it rendered to HTML.

# NAME

CInet::Seq::Propositional - Sequence of axiomatically defined relations

# SYNOPSIS

    # Define a propositional type object.
    propositional Semigraphoids = cube (ijk|L) -> (ij|L) & (ik|jL) => (ij|kL) & (ik|L);
    # Get a CInet::Seq::Propositional for its elements on a 4-element ground set:
    my $seq = Semigraphoids(4);

    # Counting is efficient and non-exhaustive using #SAT solver.
    say $seq->count;
    # Enumeration works via AllSAT solver.
    say for $seq->list;

    # Get a CInet::ManySAT solver with the axioms preloaded.
    my $solver = $seq->solver;

# DESCRIPTION

This class provides the interface of [CInet::Seq](/doc/CInet%3A%3ASeq) for collections
of axiomatically defined `CInet::Relation`s. Each instance of this
class has a backing system of axioms, which are a Boolean formula in
conjunctive normal form (CNF). Various actions on the sequence are
implemented as efficiently as possible by manipulating the axioms
and by calling into the SAT solvers from [CInet::ManySAT](/doc/CInet%3A%3AManySAT).

This class implements the [CInet::Seq](/doc/CInet%3A%3ASeq) role.

## Methods

### new

    my $prop = CInet::Propositional::Seq->new($cube, \@axioms, \&relify);

Constructs a CInet::Propositional::Seq object which iterates
`CInet::Relation` objects on the given `$cube`. The structures
contained in the sequence are encoded by the satisfying assignments
to the given `@axioms`, given in conjunctive normal form, suitable
for passing into [CInet::ManySAT](/doc/CInet%3A%3AManySAT)'s `read` method.

By default, all objects returned from this sequence are blessed
into `CInet::Relation` on the given cube. A true Boolean variable
maps to a true independence statement, so to a **0** coefficient
in the relation. This assumes that the variables are numbered
`1 .. $cube->squares`.

If you have different encodings, you can specify your own `&relify`
coderef, which receives the satisfying assignment directly from
[CInet::ManySAT](/doc/CInet%3A%3AManySAT), as an array of negated and non-negated variable
numbers. Your coderef can access the model via `$_` or `@_`.
The `$cube` is passed in as a second argument.

### axioms

    my $axioms = $prop->axioms;

Returns an arrayref of arrayrefs which represents a conjunction
of clauses. Each clause, an inner arrayref, contains positive and
negative integers, each representing a literal in the clause.

### contains

    my $bool = $prop->contains($A);

Check if the given `CInet::Relation` `$A` is in the sequence.
This does not enumerate the sequence but rather uses its defining
axioms.

## Implementation of CInet::Seq

### inhabited

    my $model = $prop->inhabited;

Returns a model if `$prop` is satisfiable and otherwise `undef`.
Unlike the vanilla [CInet::Seq#inhabited](/doc/CInet%3A%3ASeq%23inhabited) method this has no
side effects on the available elements in `$prop`, because a
separate SAT solver is started on the backing formula.

Accepts the same arguments as [CInet::ManySAT#model](/doc/CInet%3A%3AManySAT%23model).

### consistent

    my $model = $prop->consistent($partial);

Return an extension of the partially defined argument or `undef` if
the partial assignment is inconsistent. The argument does not have to
be partially defined. If it is totally defined, then this checks only
the consistency and returns a copy of the given model or `undef`.

TODO: This currently makes assumptions about an `$unrelify`
And really, `$relify` and `$unrelify` should be encapsulated
into something and be called `pack` and `unpack`. Maybe it can
be encapsulated into the Type object via mixins?

### solver

    my $solver = $prop->solver($class);

Return a SAT solver preloaded with the backing formula. The `$class`
argument specifies the class of solver to be returned. It must implement
the `CInet::ManySAT::Base` role. The default value for `$class` is
`CInet::ManySAT`.

### incremental

    my $incr = $prop->incremental;

Return an instance of [CInet::ManySAT::Incremental](/doc/CInet%3A%3AManySAT%3A%3AIncremental) loaded with the
backing formula. Such a solver can only answer consistency queries
but asking it lots of such queries is considerably faster.

### count

    my $count = $prop->count;

Return the number of elements in the sequence, which is the number
of satisfying assignments to the backing formula. Unlike the vanilla
[CInet::Seq#count](/doc/CInet%3A%3ASeq%23count) method, this does not exhaust the sequence,
because a separate #SAT solver is started on the backing formula.

Accepts the same arguments as [CInet::ManySAT#count](/doc/CInet%3A%3AManySAT%23count).

### next

    my $elt = $prop->next;
    last if not defined $elt;

Pull the next satisfying assignment of the backing formula. If not
running already, an AllSAT solver is started which carries out the
enumeration. This solver runs in a separate process and fills an
IPC buffer with new models. It is automatically put to sleep when this
fixed-size buffer is full, so no extraordinary amounts of memory will
be used in case the consumer of this Seq is slow. In addition, the
enumeration is automatically canceled when this object is destroyed.

On an invocation of this method which starts the AllSAT solver,
all arguments are forwarded to [CInet::ManySAT#all](/doc/CInet%3A%3AManySAT%23all).

# AUTHOR

Tobias Boege <tobs@taboege.de>

# COPYRIGHT AND LICENSE

This software is copyright (C) 2020 by Tobias Boege.

This is free software; you can redistribute it and/or
modify it under the terms of the Artistic License 2.0.