NAME

CInet::Alien::SharpSAT::TD - The model counter SharpSAT-TD

SYNOPSIS

use IPC::Run3;
use CInet::Alien::SharpSAT::TD qw(sharpsat_td);

# Run #SAT solver on a DIMACS CNF file.
# The tree decomposition has a timeout of 10 seconds.
run3 [sharpsat_td(10), $cnf_file], \undef, \my $out, \undef;

# Clauses produced programmatically can be sent to stdin
run3 [sharpsat_td(10)], \&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::SharpSAT::TD v1.0.0.

DESCRIPTION

This module builds a custom version of the model counter SharpSAT-TD developed by Tuukka Korhonen and Matti Järvisalo. 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::SharpSAT::TD is an Alien::Base with two additional methods:

exe

my $program = CInet::Alien::SharpSAT::TD->exe;

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

flowcutter_exe

my $program = CInet::Alien::SharpSAT::TD->flowcutter_exe;

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

EXPORTS

There is one optional export:

sharpsat_td

use CInet::Alien::SharpSAT::TD qw(sharpsat_td);
my @cmd = sharpsat_td(%opts);

Return a list of command-line words. The first is the absolute path to sharpSAT, followed by arguments assembled from the given %opts:

• Add cs => $cachesize to configure the cache size in megabytes.

• Add td => $timeout to enable the tree decomposition step and run it for the given number of seconds.

• Add tw => $weight to set the weight of the tree decomposition in the decision heuristic.

Refer to the documentation of sharpsat-td for more details.

SEE ALSO

• The original paper about SharpSAT-TD is https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.8.

• The original source code for SharpSAT-TD is on github: https://github.com/Laakeri/sharpsat-td.

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

AUTHOR

Tobias Boege <tobs@taboege.de>

COPYRIGHT AND LICENSE

This software is copyright (C) 2025 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 SharpSAT-TD solver is Copyright (c) 2021 Tuukka Korhonen who released it under the MIT license.

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

It also includes flowcutter and clhash; see the LICENSE file of SharpSAT-TD for more information.