Skip to content

Commit 6949523

Browse files
🎨 refactor: Use flat export style and improve documentation.
1 parent 171e02d commit 6949523

27 files changed

Lines changed: 242 additions & 120 deletions

src/api/decide.js

Lines changed: 17 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,20 @@
1-
import {solve} from './solve.js';
1+
import assert from 'assert';
2+
import ParitiesInstance from '../core/convert/ParitiesInstance.js';
3+
import SignsInstance from '../core/convert/SignsInstance.js';
4+
import KeysInstance from '../core/convert/KeysInstance.js';
5+
import solve from './solve.js';
26

3-
export function decide(instance) {
7+
/**
8+
* Decide whether the given instance has a satisfying assignment.
9+
*
10+
* @param {ParitiesInstance|SignsInstance|KeysInstance} instance
11+
* @return {boolean} Whether the instance has a satisfying assignment.
12+
*/
13+
export default function decide(instance) {
14+
assert(
15+
instance instanceof ParitiesInstance ||
16+
instance instanceof SignsInstance ||
17+
instance instanceof KeysInstance,
18+
);
419
return !solve(instance).next().done;
520
}

src/api/from.js

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,50 @@
1-
import {
2-
ParitiesInstance,
3-
_sign_to_parity,
4-
_keys_to_parity,
5-
_parse_DIMACS_CNF,
6-
} from '../core/index.js';
1+
import ParitiesInstance from '../core/convert/ParitiesInstance.js';
2+
import _sign_to_parity from '../core/convert/_sign_to_parity.js';
3+
import _keys_to_parity from '../core/convert/_keys_to_parity.js';
4+
import _parse_DIMACS_CNF from '../core/parse/_parse_DIMACS_CNF.js';
75

86
/**
97
* The input is converted to parity format in each case.
108
*/
11-
export const from = {
9+
const from = {
1210
/**
1311
* The input is in parity format where variables are given integer labels
1412
* 0 to n-1, a positive literal is represented by the double of its
1513
* variable's label, and a negative literal is represented by the successor
1614
* of the double of its variable's label.
15+
*
16+
* @param {number[][]} clauses The clauses in parity format.
17+
* @return {ParitiesInstance}
1718
*/
1819
parities: (clauses) => new ParitiesInstance(clauses),
1920
/**
2021
* The input is in signs format where variables are given integer labels
2122
* 1 to n, a positive literal is represented by its variable's label, and a
2223
* negative literal is represented by the opposite of its variable's label.
24+
*
25+
* @function
26+
* @param {number[][]} clauses
27+
* @return {SignsInstance}
2328
*/
2429
signs: _sign_to_parity,
2530
/**
2631
* The input is in keys format where variables are given arbitrary object labels,
2732
* a literal is represented by a pair from the set {true, false} x
2833
* labels, where the first item in the pair is true if the literal is positive,
2934
* and false otherwise.
35+
*
36+
* @function
37+
* @param {[any,any][][]} clauses
38+
* @return {KeysInstance}
3039
*/
3140
keys: _keys_to_parity,
3241
/**
3342
* Parses a character iterable in DIMACS CNF format.
43+
*
44+
* @param {Iterable<string>} iterable
45+
* @return {ParitiesInstance}
3446
*/
3547
dcnf: (iterable) => new ParitiesInstance(_parse_DIMACS_CNF(iterable)),
3648
};
49+
50+
export default from;

src/api/index.js

Lines changed: 0 additions & 4 deletions
This file was deleted.

src/api/solve.js

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,14 @@
1-
import {SAT0W, setup_watchlist, setup_assignment} from '../core/index.js';
1+
import setup_assignment from '../core/setup_assignment.js';
2+
import setup_watchlist from '../core/SAT0W/setup_watchlist.js';
3+
import SAT0W from '../core/SAT0W/SAT0W.js';
24

35
/**
46
* Yields all satisfying assignments for the input instance.
57
*
6-
* @returns {Iterable} Generator of the satisfying assignments.
8+
* @param {ParitiesInstance|SignsInstance|KeysInstance} instance
9+
* @returns {IterableIterator<number[]>} Generator of the satisfying assignments.
710
*/
8-
export function* solve({clauses, n}) {
11+
export default function solve({clauses, n}) {
912
// eslint-disable-next-line new-cap
10-
yield* SAT0W(n, clauses, setup_watchlist(n, clauses), setup_assignment(n), 0);
13+
return SAT0W(n, clauses, setup_watchlist(n, clauses), setup_assignment(n), 0);
1114
}

src/api/verify.js

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
1-
import {_verify} from '../core/index.js';
2-
export const verify = ({clauses}, certificate) => _verify(clauses, certificate);
1+
import _verify from '../core/_verify.js';
2+
const verify = ({clauses}, certificate) => _verify(clauses, certificate);
3+
export default verify;

src/core/SAT0W/SAT0W.js

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,20 @@
1-
import {update_watchlist} from './update_watchlist.js';
1+
import update_watchlist from './update_watchlist.js';
22

3-
export function* SAT0W(n, clauses, watchlist, assignment, d) {
4-
/**
5-
* Recursively solve SAT by assigning to variables d, d+1, ..., n-1. Assumes
6-
* variables 0, ..., d-1 are assigned so far. A generator for all the
7-
* satisfying assignments is returned.
8-
*/
3+
/**
4+
* SAT0W.
5+
*
6+
* Recursively solve SAT by assigning to variables d, d+1, ..., n-1. Assumes
7+
* variables 0, ..., d-1 are assigned so far. A generator for all the
8+
* satisfying assignments is returned.
9+
*
10+
* @param {number} n
11+
* @param {number[][]} clauses
12+
* @param {number[][][]} watchlist
13+
* @param {number[]} assignment
14+
* @param {number} d
15+
* @return {IterableIterator<number[]>} Yields satisfying assignments.
16+
*/
17+
export default function* SAT0W(n, clauses, watchlist, assignment, d) {
918
if (d === n) {
1019
yield assignment;
1120
return;

src/core/SAT0W/index.js

Lines changed: 0 additions & 3 deletions
This file was deleted.

src/core/SAT0W/setup_watchlist.js

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,11 @@
1-
export function setup_watchlist(n, clauses) {
1+
/**
2+
* Setup_watchlist.
3+
*
4+
* @param {number} n
5+
* @param {number[][]} clauses
6+
* @return {number[][][]} The literal watch list.
7+
*/
8+
export default function setup_watchlist(n, clauses) {
29
const watchlist = [];
310

411
for (let i = 0; i < 2 * n; ++i) watchlist.push([]);

src/core/SAT0W/update_watchlist.js

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,14 @@
1-
export function update_watchlist(watchlist, false_literal, assignment) {
2-
/**
3-
* Updates the watch list after literal 'false_literal' was just assigned
4-
* False, by making any clause watching false_literal watch something else.
5-
* Returns False it is impossible to do so, meaning a clause is contradicted
6-
* by the current assignment.
7-
*/
1+
/**
2+
* Updates the watch list after literal 'false_literal' was just assigned
3+
* False, by making any clause watching false_literal watch something else.
4+
* Returns False it is impossible to do so, meaning a clause is contradicted
5+
* by the current assignment.
6+
*
7+
* @param {number[][][]} watchlist
8+
* @param {number} false_literal
9+
* @param {number[]} assignment
10+
*/
11+
export default function update_watchlist(watchlist, false_literal, assignment) {
812
while (watchlist[false_literal].length > 0) {
913
const clause =
1014
watchlist[false_literal][watchlist[false_literal].length - 1];

src/core/_verify.js

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88
* @returns {Boolean} Whether the assignment satisfies the k-CNF formula
99
* represented by the list of clauses.
1010
*/
11-
export function _verify(clauses, assignment) {
11+
export default function _verify(clauses, assignment) {
1212
// eslint-disable-next-line no-labels
1313
loop: for (const clause of clauses) {
1414
for (const literal of clause) {

0 commit comments

Comments
 (0)