Home Manual Reference Source

References

api

summary
public	F decide(instance: ParitiesInstance \| SignsInstance \| KeysInstance): boolean Decide whether the given instance has a satisfying assignment.
public	F solve(instance: ParitiesInstance \| SignsInstance \| KeysInstance): IterableIterator<number[]> Yields all satisfying assignments for the input instance.
public	F verify(instance: ParitiesInstance \| SignsInstance \| KeysInstance, certificate: number[]): boolean Verify that satisfiability of the input instance can be derived from the input certificate.
public	V from_: {"parities": , "signs": , "keys": , "dcnf": } The input is converted to parity format in each case.

core

summary
private	F _verify(clauses: number[][], assignment: number[]): boolean Verifies that an assignment vector satisfies a k-CNF formula given as a list of clauses.
public	F setup_assignment(n: number): number[] Setup_assignment.

core/SAT0W

summary
public	F * SAT0W(n: number, clauses: number[][], watchlist: number[][][], assignment: number[], d: number): IterableIterator<number[]> SAT0W.
public	F setup_watchlist(n: number, clauses: number[][]): number[][][] Setup_watchlist.
public	F 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.

core/convert

summary
public	C KeysInstance Maintains a mapping between variable names and a parity representation of the instance.
public	C ParitiesInstance Holds all properties of a k-CNF SAT instance in parity format.
public	C SignsInstance Allows to produce an assignment format that makes sense in sign format.
private	F _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	F _count(clauses: number[][]): number Counts the number of variables in a parity format clauses list.
private	F _keys_to_parity(clauses: [any,any][][]): KeysInstance _keys_to_parity.
private	F _parity_to_keys(variables: any[], clauses: number[][]): * _parity_to_keys.
private	F _parity_to_sign(clauses: number[][]): number[][] _parity_to_sign.
private	F _sign_to_parity(clauses: number[][]): SignsInstance _sign_to_parity.

core/parse

summary
private	F _parse_DIMACS_CNF(iterable: Iterable<string>): * _parse_DIMACS_CNF.
private	F _parse_int(first_symbol: string, iterator: Iterator<string>): [boolean, number] _parse_int.
private	F _skip_blanks(iterator: Iterator<string>): [boolean, string] _skip_blanks.

Directories