NAME

CInet::Alien::GANAK - The probabilistic model counter GANAK

SYNOPSIS

use IPC::Run3;
use CInet::Alien::GANAK qw(ganak);

# Run #SAT solver on a DIMACS CNF file
run3 [ganak, $cnf_file], \undef, \my $out, \undef;

# Clauses produced programmatically can be sent to stdin
run3 [ganak], \&produce_clauses, \my $out, \undef;

# In any case, parse the answer from $out.
# CAUTION: it may overflow Perl's native integer,
# consider C<use bignum>.
my ($count,) = $out =~ /^s mc (\d+)/m;

VERSION

This document describes CInet::Alien::GANAK v1.0.0.

DESCRIPTION

This module builds a custom version of the probabilistic exact model counter GANAK developed by Meel and collaborators. It takes a Boolean formula in conjunctive normal form (in the DIMACS CNF format) and produces the number of satisfying assignments to it. It is correct with a certain, adjustable probability. It may fail to terminate with a conclusive answer as well.

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

exe

my $program = CInet::Alien::GANAK->exe;

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

EXPORTS

There is one optional export:

ganak

use CInet::Alien::GANAK qw(ganak);
my $program = ganak;

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

SEE ALSO

• The original paper about GANAK is https://www.comp.nus.edu.sg/~meel/Papers/ijcai19srsm.pdf.

• The original source code for ganak is on github: https://github.com/meelgroup/ganak.

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

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.

Bundled software

The GANAK solver is Copyright (C) 2018 by Shubham Sharma, Subhajit Roy, Mate Soos and Kuldeep S. Meel who released it under the MIT license.

Parts of GANAK are based on sharpSAT which is Copyright (C) 2012 by Marc Thurley and released under the MIT license.

Our modifications in particular replace usage of the GMP library by BigInt which is Copyright (C) 2019 Syed Faheel Ahmad who released it under the MIT license.