Function

Static Public Summary
public	* SAT0W(n: number, clauses: number[][], watchlist: number[][][], assignment: number[], d: number): IterableIterator<number[]> SAT0W.
public	decide(instance: ParitiesInstance \| SignsInstance \| KeysInstance): boolean Decide whether the given instance has a satisfying assignment.
public	setup_assignment(n: number): number[] Setup_assignment.
public	setup_watchlist(n: number, clauses: number[][]): number[][][] Setup_watchlist.
public	solve(instance: ParitiesInstance \| SignsInstance \| KeysInstance): IterableIterator<number[]> Yields all satisfying assignments for the input instance.
public	update_watchlist(watchlist: number[][][], false_literal: number, assignment: number[]): boolean Updates the watch list after literal 'false_literal' was just assigned False, by making any clause watching false_literal watch something else.
public	verify(instance: ParitiesInstance \| SignsInstance \| KeysInstance, certificate: number[]): boolean Verify that satisfiability of the input instance can be derived from the input certificate.

Static Private Summary
private	_certificate_to_keys(variables: any[], certificate: number[]): Map<any, number> Constructs an assignment map from a list of variable names and an assignment vector in parity format.
private	_count(clauses: number[][]): number Counts the number of variables in a parity format clauses list.
private	_keys_to_parity(clauses: [any,any][][]): KeysInstance _keys_to_parity.
private	_parity_to_keys(variables: any[], clauses: number[][]): * _parity_to_keys.
private	_parity_to_sign(clauses: number[][]): number[][] _parity_to_sign.
private	_parse_DIMACS_CNF(iterable: Iterable<string>): * _parse_DIMACS_CNF.
private	_parse_int(first_symbol: string, iterator: Iterator<string>): [boolean, number] _parse_int.
private	_sign_to_parity(clauses: number[][]): SignsInstance _sign_to_parity.
private	_skip_blanks(iterator: Iterator<string>): [boolean, string] _skip_blanks.
private	_verify(clauses: number[][], assignment: number[]): boolean Verifies that an assignment vector satisfies a k-CNF formula given as a list of clauses.

Static Public

public * SAT0W(n: number, clauses: number[][], watchlist: number[][][], assignment: number[], d: number): IterableIterator<number[]> source

import SAT0W from '@problem-solving/sat/src/core/SAT0W/SAT0W.js'

SAT0W.

Recursively solve SAT by assigning to variables d, d+1, ..., n-1. Assumes variables 0, ..., d-1 are assigned so far. A generator for all the satisfying assignments is returned.

Params:

Name	Type	Attribute	Description
n	number
clauses	number[][]
watchlist	number[][][]
assignment	number[]
d	number

Return:

IterableIterator<number[]>

Yields satisfying assignments.

public decide(instance: ParitiesInstance | SignsInstance | KeysInstance): boolean source

import decide from '@problem-solving/sat/src/api/decide.js'

Decide whether the given instance has a satisfying assignment.

Params:

Name	Type	Attribute	Description
instance	ParitiesInstance \| SignsInstance \| KeysInstance

Return:

boolean

Whether the instance has a satisfying assignment.

public setup_assignment(n: number): number[] source

import setup_assignment from '@problem-solving/sat/src/core/setup_assignment.js'

Setup_assignment.

Params:

Name	Type	Attribute	Description
n	number

Return:

number[]

public setup_watchlist(n: number, clauses: number[][]): number[][][] source

import setup_watchlist from '@problem-solving/sat/src/core/SAT0W/setup_watchlist.js'

Setup_watchlist.

Params:

Name	Type	Attribute	Description
n	number
clauses	number[][]

Return:

number[][][]

The literal watch list.

public solve(instance: ParitiesInstance | SignsInstance | KeysInstance): IterableIterator<number[]> source

import solve from '@problem-solving/sat/src/api/solve.js'

Yields all satisfying assignments for the input instance.

Params:

Name	Type	Attribute	Description
instance	ParitiesInstance \| SignsInstance \| KeysInstance

Return:

IterableIterator<number[]>

Generator of the satisfying assignments.

public update_watchlist(watchlist: number[][][], false_literal: number, assignment: number[]): boolean source

import update_watchlist from '@problem-solving/sat/src/core/SAT0W/update_watchlist.js'

Updates the watch list after literal 'false_literal' was just assigned False, by making any clause watching false_literal watch something else. Returns False it is impossible to do so, meaning a clause is contradicted by the current assignment.

Params:

Name	Type	Attribute	Description
watchlist	number[][][]
false_literal	number
assignment	number[]

Return:

boolean

public verify(instance: ParitiesInstance | SignsInstance | KeysInstance, certificate: number[]): boolean source

import verify from '@problem-solving/sat/src/api/verify.js'

Verify that satisfiability of the input instance can be derived from the input certificate.

Params:

Name	Type	Attribute	Description
instance	ParitiesInstance \| SignsInstance \| KeysInstance
certificate	number[]

Return:

boolean

Static Private

private _certificate_to_keys(variables: any[], certificate: number[]): Map<any, number> source

import _certificate_to_keys from '@problem-solving/sat/src/core/convert/_certificate_to_keys.js'

Constructs an assignment map from a list of variable names and an assignment vector in parity format.

Params:

Name	Type	Attribute	Description
variables	any[]
certificate	number[]

Return:

Map<any, number>

private _count(clauses: number[][]): number source

import _count from '@problem-solving/sat/src/core/convert/_count.js'

Counts the number of variables in a parity format clauses list.

Params:

Name	Type	Attribute	Description
clauses	number[][]		The clauses list in parity format.

Return:

number

The number of variables in the clauses list.

private _keys_to_parity(clauses: [any,any][][]): KeysInstance source

import _keys_to_parity from '@problem-solving/sat/src/core/convert/_keys_to_parity.js'

_keys_to_parity.

Params:

Name	Type	Attribute	Description
clauses	[any,any][][]

Return:

KeysInstance

private _parity_to_keys(variables: any[], clauses: number[][]): * source

import _parity_to_keys from '@problem-solving/sat/src/core/convert/_parity_to_keys.js'

_parity_to_keys.

Params:

Name	Type	Attribute	Description
variables	any[]
clauses	number[][]

Return:

private _parity_to_sign(clauses: number[][]): number[][] source

import _parity_to_sign from '@problem-solving/sat/src/core/convert/_parity_to_sign.js'

_parity_to_sign.

Params:

Name	Type	Attribute	Description
clauses	number[][]

Return:

number[][]

private _parse_DIMACS_CNF(iterable: Iterable<string>): * source

import _parse_DIMACS_CNF from '@problem-solving/sat/src/core/parse/_parse_DIMACS_CNF.js'

_parse_DIMACS_CNF.

Params:

Name	Type	Attribute	Description
iterable	Iterable<string>

Return:

private _parse_int(first_symbol: string, iterator: Iterator<string>): [boolean, number] source

import _parse_int from '@problem-solving/sat/src/core/parse/_parse_int.js'

_parse_int.

Params:

Name	Type	Attribute	Description
first_symbol	string
iterator	Iterator<string>

Return:

[boolean, number]

private _sign_to_parity(clauses: number[][]): SignsInstance source

import _sign_to_parity from '@problem-solving/sat/src/core/convert/_sign_to_parity.js'

_sign_to_parity.

Params:

Name	Type	Attribute	Description
clauses	number[][]

Return:

SignsInstance

private _skip_blanks(iterator: Iterator<string>): [boolean, string] source

import _skip_blanks from '@problem-solving/sat/src/core/parse/_skip_blanks.js'

_skip_blanks.

Params:

Name	Type	Attribute	Description
iterator	Iterator<string>

Return:

[boolean, string]

private _verify(clauses: number[][], assignment: number[]): boolean source

import _verify from '@problem-solving/sat/src/core/_verify.js'

Verifies that an assignment vector satisfies a k-CNF formula given as a list of clauses. The list of clauses and the assignment vector are in parity format.

Params:

Name	Type	Attribute	Description
clauses	number[][]		The clauses in parity format.
assignment	number[]		The assignment vector in parity format.

Return:

boolean

Whether the assignment satisfies the k-CNF formula represented by the list of clauses.