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::ManySAT - A collection of SAT solvers

# SYNOPSIS

    # Add clauses to a new solver
    my $solver = CInet::ManySAT->new->read($cnf);

    # Check satisfiability, obtain a witness
    my $model = $solver->model;
    say join(" ", $model->@*) if defined $model;

    # Count satisfying assignments
    say $solver->count(risk => 0.05);   # probably exact count with 5% risk
    say $solver->count([-2]);  # exact count of all models where 2 is false

    # Enumerate all satisfying assignments
    my $all = $solver->all;
    while (defined(my $model = $all->next)) {
        say join(" ", $model->@*);
        $all->cancel and last if ++$count > $caring_for;
    }

## VERSION

This document describes CInet::ManySAT v1.1.0.

# DESCRIPTION

`CInet::ManySAT` provides a common interface to a variety of solvers for
the Boolean satisfiability problem (SAT) and its variants.

The supported SAT-like problems are described in the next sections. They all
operate on a Boolean formula presented in conjunctive normal form (CNF).
The solvers used internally are heterogenous, independent programs. Therefore
this class does the [CInet::ManySAT::ClauseStorage](/doc/CInet%3A%3AManySAT%3A%3AClauseStorage) role to provide a common
formula storage mechanism for all of them. See the documentation of that role
for how to read a formula into the solver or how to get it back out in the
standard DIMACS CNF format.

## Satisfiability and consistency checking

In its simplest form, SAT is about deciding whether a Boolean formula has
a solution, that is an assignment of true and false to the variables which
_satisfies_ all the clauses of the formula simultaneously. The SAT solver
is available through the [model](#model) method which returns either a
_model_ of the formula or `undef` if the formula is not satisfiable. In this
documentation, the word "model" is used for "satisfying assignment".
Thus the [model](#model) method is a witnessing SAT solver, in that it
provides you with a witness for the "SAT" answer (but not the "UNSAT" answer).

The [model](#model) method accepts optional _assumptions_. These come in the
form of an arrayref of non-zero integers, just like the clauses of the formula.
The assumptions fix the truth value of some of the variables and they are
valid only for the current invocation of the solver. In this way, you can
use the solver to check if an assignment is _consistent_ with the formula,
that is whether this partial assignment can be extended to a satisfying one.
It can also be used to simply evaluate the formula, verifying that a full
assignment is actually a model.

### Low-overhead incremental solver

If your problem requires checking the same formula over and over again on
different sets of assumptions (maybe because you want to compute a projection
of the set of satisfying assignments to your formula), the solver contained
in this class will not make you very happy. Since `CInet::ManySAT` has to
support a range of different solvers, it writes a temporary DIMACS CNF file
for every solver invocation, which slows down any large loop around them.
You should consider using the [CInet::ManySAT::Incremental](/doc/CInet%3A%3AManySAT%3A%3AIncremental) solver, which
is specialized to those tasks.

## Model counting

We provide two **#SAT solvers**. Such a solver determines the number of
satisfying assignments to a formula, potentially faster than by iterating
over them all. One of the solvers is exact and the other is probabilistically
exact, meaning that it delivers the correct answer only with a configurable
probability. The probabilistic solver is generally faster but it may give
up on the formula entirely if it finds that it cannot guarantee exactness
with the given probability. These solvers are accessible through the [count](#count)
method with its optional `risk` parameter.

## Model enumeration

After producing a single model and counting all models, the last task
supported is to enumerate all models. This problem is known as **AllSAT**.
This module provides an interface to a solver which lazily produces all
the models of a formula. The solver usually starts outputting models
immediately (if it can find them) but gets put to sleep by the operating
system when the IPC buffer is filled up. This way, a slow application
processing the models does not cause the solver to fill up extraordinary
amounts of memory nor the solver to "run away" but maintain a reasonably
full pool of models for immediate reading. The enumeration is cancelable.

## Methods

### new

    my $solver = CInet::ManySAT::Count->new;

Create a new instance of a ManySAT solver. Use `read` and `add` of
[CInet::ManySAT::ClauseStorage](/doc/CInet%3A%3AManySAT%3A%3AClauseStorage) to fill it with clauses.

### model

    my $model = $solver->model($assump);
    say join(' ', $model->@*) if defined $model;

    say "consistent" if $solver->model($assignment);

Checks the formula for satisfiability and returns a witness model in case
it is satisfiable. Otherwise returns `undef`. If the solver gave up or
terminated abnormally, an exception is raised.

The first argument `$assump` is an optional arrayref defining the values
of some of the variables for the current run only. Therefore this method
can be used for model checking or consistency checking as well.

### count

    say $solver->count($assump);
    say $solver->count($assump, risk => 0.05); # probably correct

Exactly count the models of the formula stored in the solver.

The first argument `$assump` is an optional arrayref defining the values
of some of the variables for the current run only.

The remaining arguments are treated as options. The only supported option
currently is `risk`. If specified with a non-zero probability, it causes
the probabilistically exact solver to be invoked.

This method raises an error if the solver terminated abnormally.

### all

    say for $solver->all($assump)->list;
    say for $all->list;

    # Or more memory-friendly:
    while (defined(my $model = $all->next)) {
        say $model;
        $all->cancel and last if had_enough;
    }

Enumerate all models of the formula stored in the solver.

The first argument `$assump` is an optional arrayref defining the values
of some of the variables for the current run only.

This method returns an object of type [CInet::ManySAT::All](/doc/CInet%3A%3AManySAT%3A%3AAll) which can be
used to control the enumeration.

## EXPORTS

The following functions are exported on demand:

    my $model = sat_model ($cnf, $assump, %opts);
    my $count = sat_count ($cnf, $assump, %opts);
    my $all   = sat_all   ($cnf, $assump, %opts);

Each `sat_$action($cnf, @_)` is equivalent to `CInet::ManySAT->new->read($cnf)->$action(@_)`.

# 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.