diff --git a/test/src/SAT.js b/test/src/SAT.js index 93e65ac..78de393 100644 --- a/test/src/SAT.js +++ b/test/src/SAT.js @@ -2,7 +2,7 @@ import test from 'ava'; import * as sat from '../../src/index.js'; import * as compare from '@aureooms/js-compare'; -import {list} from '@aureooms/js-itertools'; +import {list, map} from '@aureooms/js-itertools'; const lex = compare.lexicographical(compare.increasing); @@ -77,3 +77,32 @@ test('#2', (t) => { ['C', 1], ]); }); + +test('#3', (t) => { + const instance = sat.from.signs([ + [-1, 2, 3], + [-2, -4, 5], + [1, -5], + ]); + const satisfying_assignments = list( + map((certificate) => instance.assignment(certificate), sat.solve(instance)), + ); + t.deepEqual(satisfying_assignments, [ + [0, 0, 0, 0, 0, 0], + [0, 0, 0, 0, 1, 0], + [0, 0, 0, 1, 0, 0], + [0, 0, 0, 1, 1, 0], + [0, 0, 1, 0, 0, 0], + [0, 0, 1, 1, 0, 0], + [0, 1, 0, 1, 0, 0], + [0, 1, 0, 1, 0, 1], + [0, 1, 0, 1, 1, 0], + [0, 1, 0, 1, 1, 1], + [0, 1, 1, 0, 0, 0], + [0, 1, 1, 0, 0, 1], + [0, 1, 1, 0, 1, 1], + [0, 1, 1, 1, 0, 0], + [0, 1, 1, 1, 0, 1], + [0, 1, 1, 1, 1, 1], + ]); +});