Usage
The code needs a ES2015+ polyfill to work, for example regenerator-runtime/runtime.
await import( 'regenerator-runtime/runtime.js' ) ;
// or
import 'regenerator-runtime/runtime.js' ;
Then
const sat = await import( '@problem-solving/sat' ) ;
// or
import * as sat from '@problem-solving/sat' ;
Example
import { lexicographical } from '@total-order/lex' ;
import { increasing } from '@total-order/primitive' ;
import { list } from '@iterable-iterator/list' ;
const lex = lexicographical( increasing ) ;
const instance = sat.from.keys( [
[ [ 1 , 'A' ] , [ 1 , 'B' ] , [ 0 , 'C' ] ] ,
[ [ 1 , 'B' ] , [ 1 , 'C' ] ] ,
[ [ 0 , 'B' ] ],
[ [ 0 , 'A' ] , [ 1 , 'C' ] ]
] ) ;
const certificates = sat.solve( instance ) ;
const state = certificates.next( ) ;
const certificate = state.value ;
sat.verify( instance , certificate ) ; // true
sat.decide( instance ) ; // true
state.done ; // false
const assignment = instance.assignment( certificate ) ;
list( assignment.entries( ) ).sort( lex ) ; // [ [ 'A' , 1 ] , [ 'B' , 0 ] , [ 'C' , 1 ] ]
certificates.next( ).done ; // true
const text = "p cnf 30 4\n10 0 10 20 30\n0\n-10 -20\n-30 0 10 -20 30" ;
const instance = sat.from.dcnf( text ) ;
instance.n ; // 30
instance.clauses ; // [ [ 18 ] , [ 18 , 38 , 58 ] , [ 19 , 39 , 59 ] , [ 18 , 39 , 58 ] ]
const filename = 'uf20-010.cnf' ;
const iterable = fs.readFileSync( filename , { encoding : 'utf8' } ) ;
const instance = sat.from.dcnf( iterable ) ;