*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](/doc/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](/doc/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](/doc/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](/doc/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.