CInet::ManySAT - A collection of SAT solvers
# 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;
}This document describes CInet::ManySAT v1.1.0.
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 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.
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 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 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 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.
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 solver, which is specialized to those tasks.
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 method with its optional risk parameter.
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.
my $solver = CInet::ManySAT::Count->new;Create a new instance of a ManySAT solver. Use read and add of CInet::ManySAT::ClauseStorage to fill it with clauses.
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.
say $solver->count($assump);
say $solver->count($assump, risk => 0.05); # probably correctExactly 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.
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 which can be used to control the enumeration.
my $str = $solver->description;Returns a human-readable description of the object.
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(@_).
Tobias Boege <tobs@taboege.de>
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.