NAME

CInet::Alien::MiniSAT::All - The AllSAT solver nbc_minisat_all

SYNOPSIS

use IPC::Run3;
use CInet::Alien::MiniSAT::All qw(nbc_minisat_all);

# Run AllSAT solver on a DIMACS CNF file, process each model in &take_model
run3 [nbc_minisat_all, $cnf_file], \undef, \&take_model, \undef;

# Clauses produced programmatically can be sent to stdin
run3 [nbc_minisat_all], \&produce_clauses, \&take_model, \undef;

VERSION

This document describes CInet::Alien::MiniSAT::All v1.0.0.

DESCRIPTION

This module builds a custom version of Takahisa Toda and Takehide Soh's AllSAT solver nbc_minisat_all. The nbc variant of their solvers uses a backtracking algorithm to enumerate all solutions to a Boolean formula in conjunctive normal form. Because of the backtracking, it can start producing models right away (without a knowledge compilation step) and its memory consumption stays at bay (unlike a blocking-clause-based algorithm). It is especially suitable for enumerations of moderate sizes and where the consumer wants a steady stream of models.

The package CInet::Alien::MiniSAT::All is an Alien::Base with one additional method:

exe

my $program = CInet::Alien::MiniSAT::All->exe;

Returns the absolute path of the nbc_minisat_all executable bundled with this module.

Note that the basename of this path is not guaranteed to be exactly nbc_minisat_all. It may have a custom suffix like _static.

EXPORTS

There is one optional export:

nbc_minisat_all

use CInet::Alien::MiniSAT::All qw(nbc_minisat_all);
my $program = nbc_minisat_all;

Returns the same path as exe but is shorter to type.

SEE ALSO

• The academic paper about the AllSAT solvers developed by Toda and Soh is https://dl.acm.org/doi/10.1145/2975585.

• The original source code for nbc_minisat_all is on Takahisa Toda's website http://www.sd.is.uec.ac.jp/toda/code/nbc_minisat_all.html.

• The source code repository of the fork bundled with this module is https://github.com/taboege/nbc_minisat_all.

AUTHOR

Tobias Boege <[email protected]>

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.

Bundled software

The nbc_minisat_all solver is Copyright (C) 2015 by Takahisa Toda who released it under the MIT license.

Toda's work is based on minisat which is Copyright (C) 2005 by Niklas Een and Niklas Sorensson who released it under the MIT license.