NAME

CInet::Alien::DSHARP - The model counter DSHARP

SYNOPSIS

use IPC::Run3;
use CInet::Alien::DSHARP qw(dsharp);

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

# Clauses produced programmatically can be sent to stdin
run3 [dsharp], \&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 =~ /^#SAT.* (\d+)$/;

VERSION

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

DESCRIPTION

This module builds a custom version of the model counter DSHARP developed by Muise, McIlraith, Beck and Hsu. It takes a Boolean formula in conjunctive normal form (in the DIMACS CNF format) and produces the number of satisfying assignments to it.

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

exe

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

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

EXPORTS

There is one optional export:

dsharp

use CInet::Alien::DSHARP qw(dsharp);
my $program = dsharp;

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

SEE ALSO

• The original paper about DSHARP is https://doi.org/10.1007/978-3-642-30353-1_36.

• The original source code for dsharp is on github: https://github.com/QuMuLab/dsharp.

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

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 DSHARP solver is Copyright (C) 2012 by Christian Muise and collaborators who released it under the GPLv2 license.

Parts of DSHARP 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.