head


unit module Test::SAT;

use Test;
use Compress::Zlib;

sub maybe-gzipped ($file) {
    $file.ends-with(".gz") ??
        gzslurp($file) !! $file.IO;
}

#| Verify that the SAT::Solver in $*SAT-SOLVER makes accurate decisions.
sub sat-ok ($p (IO() :key($file), :value($answer))) is export {
    my $cnf = $file.&maybe-gzipped;
    my $yesno = $*SAT-SOLVER.new.solve: $cnf, :now;
    is $yesno, $answer, "correct decision for $file";
}

#|« Verify that the certifying SAT::Solver in $*SAT-SOLVER makes accurate
decisions and that the witness it outputs is a satisfying assignment.
»
sub witness-ok ($p (IO() :key($file), :value($answer))) is export {
    subtest "$file" => {
        plan 2;
        my $cnf = $file.&maybe-gzipped;
        my $yesno = $*SAT-SOLVER.new.solve: $cnf, my $witness, :now;
        is $yesno, $answer, "correct decision";
        if $yesno {
            if $witness.DEFINITE {
                is eval-DIMACS($cnf, $witness), $yesno, "consistent witness";
            }
            else {
                flunk "witness not delivered";
            }
        }
        else {
            pass "no short witness required for UNSAT";
        }
    }
}

sub eval-DIMACS ($file, $assignment) {
    $file = $file.IO.e ?? $file.IO !! $file;
    for $file.lines {
        next unless m/^ '-'? \d /;
        my $lits = set((m:g/ '-'? \d+ /)».Int) ∖ 0;
        return False if $assignment ∩ $lits === ∅;
    }
    return True;
}

#| Verify that the SAT::Counter in $*SAT-COUNTER produces accurate counts.
sub count-ok ($p (:key($file), :value($answer))) is export {
    my $cnf = $file.&maybe-gzipped;
    my $models = $*SAT-COUNTER.new.count: $cnf, :now;
    is $models, $answer, "correct count for $file";
}

#|« Verify that the SAT::Enumerator in $*SAT-ENUMERATOR produces the same
satisfying assignments as predicted.
»
sub enumerate-ok (
    $p (IO() :key($file), Set() :value($list)),
    &transform = { $^x },
) is export {
    subtest "$file" => {
        plan 2;
        my $cnf = $file.&maybe-gzipped;
        my @sat = $*SAT-ENUMERATOR.new.enumerate: $cnf, :now;
        is +@sat, $list.elems, "same number of answers"; # in particular no duplications!
        is-deeply @sat.map(&transform).Set, $list, "assignments match";
    }
}



This library is free software; you can redistribute it and/or modify it
under the Artistic License 2.0.


root

DRMAA

React

=begin React :component<HeaderCol> :id<menu> 
=para L<Documentation|/doc/introduction>
=para L<Modules| /mods>
=para L<Examples| file:../examples/index.podlite>
=para L<Download |file:../download/index.podlite>
=para L<About|file:../about/index.podlite>
=para 🔍 K<⌘K>/K<ctrl-K>
=end React


=begin React :component<HeaderCol> :id<footer>  
=begin nested :!nested
=item1 B<Language>
    =item2 L<Get started|file:../getting-started/getting-started.podlite>
    =item2 L<Why Raku?|/doc/language/faq#Why-should-I-learn-Raku-What's-so-great-about-it>
    =item2 L<Try Raku|https://glot.io/new/raku>
    =item2 L<Raku cheat sheet|https://github.com/Raku/mu/blob/master/docs/Perl6/Cheatsheet/cheatsheet.txt>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<Raku on Exercism|https://exercism.org/tracks/raku>
    =item2 L<Wikipedia|https://en.wikipedia.org/wiki/Raku_(programming_language)>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>

=end nested
=begin nested :!nested

=item1 B<L<Documentation|/doc>>
    =item2 L<Getting started, Migration guides from other languages, & Tutorials | file:../doc/introduction.podlite>
    =item2 L<Language References|file:../doc/reference.podlite>
    =item2 L<Type Reference| file:../doc/types.podlite>
    =item2 L<Miscellaneous| file:../doc/miscellaneous.podlite>
    =item2 L<FAQs (Frequently Asked Questions)|/doc/language/faq>
    =item2 L<Community|/doc/language/community>
    =item2 L<The list of all documents|file:../doc/index.podlite>

=item1 B<Resources>
    =item2 L<The Raku Guide|https://raku.guide/>
    =item2 L<Books |https://perl6book.com/>
    =item2 L<Rosetta Code | https://www.raku.org/community/rosettacode>

=end nested
=begin nested :!nested

=item1 B<Resoures>
    =item2 L<Download | file:../download/index.podlite>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>

=item1 B<Learning>
    =item2 L<The Raku Guide|https://raku.guide/>
    =item2 L<Wikibook |https://en.wikibooks.org/wiki/Raku_Programming>
    =item2 L<Books |https://perl6book.com/>
    =item2 L<Rosetta Code | https://www.raku.org/community/rosettacode>
    =item2 L<Learn Raku in Y minutes|https://learnxinyminutes.com/docs/raku/>
    =item2 L<Golfing |https://github.com/AlexDaniel/raku-golf-cheatsheet>
=end nested
=begin nested :!nested

=item1 B<Explore>
    =item2 L<Raku Blog Aggregator|https://planet.raku.org/>
    =item2 L<Rakudo Weekly|https://rakudoweekly.blog/>
    =item2 L<The Weekly Challenge |https://perlweeklychallenge.org/>
    =item2 L<Raku Advent Calendar|https://raku-advent.blog/>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>
    =item2 L<empty|#>

=end nested
=end React


=begin React :component<CookieConsent> :id<CookieConsent> :buttonCaption("Got it!")
=para
This website uses cookies for analytics.
=end React


SAT

NAME

SYNOPSIS

DESCRIPTION

AUTHOR

COPYRIGHT AND LICENSE