The avatar for @71
Grégoire Geis
'G' == 71
Published
Articles
Edited
Jul 6, 2020
5 stars
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
display(imply('x', 'y'))
Insert cell
Insert cell
display(xor('x', 'y', 'z'))
Insert cell
Insert cell
Insert cell
Insert cell
viewof example = display(or(and('a', 'b'), and('c', 'd'), not(and('e', not('f')))))
Insert cell
Insert cell
Insert cell
function cnf(f) {
// 1.
if (f.type === 'neg') {
if (f.clause.type === 'neg')
return cnf(f.clause);
if (f.clause.type === 'conjunct')
return cnf(or(...f.clause.clauses.map(not)));
if (f.clause.type === 'disjunct')
return cnf(and(...f.clause.clauses.map(not)));

return and(or(f));
}

// 2.
if (f.type === 'conjunct') {
return and(...f.clauses.flatMap(t => cnf(t).clauses));
}

// 3.
if (f.type === 'disjunct') {
// This is a little trickier than in the example above because 'disjunct'
// nodes may have an arbitrary number of clauses.
const clauses = [];

// Given:
// - `cnfs`, the CNFs of the subclauses,
// - `k`, the index of the CNF to process,
// - `path`, the addition of all the subclauses for a result,
// - `output`, a reference to the variable `clauses` above,
// computes the Cartesian product of the input CNFs and outputs it to `clauses`.
function build(cnfs, k, path, output) {
if (k === cnfs.length) {
const flattened_path = [];

for (const clause of path) {
if (clause.type === 'disjunct')
flattened_path.push(...clause.clauses);
else
flattened_path.push(clause);
}

return output.push(or(...flattened_path));
}

const input = cnfs[k].clauses;

for (let i = 0; i < input.length; i++) {
path[k] = input[i];

build(cnfs, k + 1, path, output);
}
}

build(f.clauses.map(cnf), 0, Array.from({ length: f.clauses.length }), clauses);

return and(...clauses);
}

// 4.
return and(or(f));
}
Insert cell
Insert cell
viewof example_cnf = display(cnf(example))
Insert cell
Insert cell
Insert cell
class Variable {
constructor(name) {
this.name = name;
this.unassign();
}

/**
* Assigns a value to the variable, given the decision level of the assignment
* and the antecedent of the assignment (the clause thanks to which this
* assignment was inferred, or null if this is an arbitrary assignment).
*/
assign(value, decision_level, antecedent = null) {
this.value = value;
this.is_assigned = true;
this.decision_level = decision_level;
this.antecedent = antecedent;
}

/**
* Unassigns the variable because its assignment was made as the result of a
* decision that ended up being incorrect.
*/
unassign() {
this.value = -1;
this.is_assigned = false;
this.decision_level = -1;
this.antecedent = null;
}
}
Insert cell
class Clause {
constructor(literals, polarity) {
// We define three constants here, for use in `compute_state` and
// `find_unique_unassigned_variable`.
Clause.SATISFIED = -1;
Clause.NORMAL = -2;
Clause.UNSATISFIED = -3;

this.literals = literals;
this.polarity = polarity;
}

/**
* Returns whether the clause is:
* - SATISFIED (at least one literal is true);
* - UNSATISFIED (all literals are false);
* - NORMAL (at least one variable is unassigned and no literal is true).
*/
compute_state() {
for (let i = 0; i < this.literals.length; i++) {
const literal = this.literals[i];

if (!literal.is_assigned)
return Clause.NORMAL;
if (literal.value === this.polarity[i])
return Clause.SATISFIED;
}

return Clause.UNSATISFIED;
}

/**
* If this clause contains a single unassigned variable, returns its index.
* Otherwise, returns if the clause is SATISFIED, UNSATISFIED or NORMAL.
*/
find_unique_unassigned_variable() {
let possible_literal_index = Clause.UNSATISFIED;

for (let i = 0; i < this.literals.length; i++) {
const literal = this.literals[i];

if (literal.is_assigned) {
if (literal.value === this.polarity[i])
return Clause.SATISFIED;
} else if (possible_literal_index === Clause.UNSATISFIED) {
possible_literal_index = i;
} else {
// We found another unassigned literal, so the clause is not unit.
return Clause.NORMAL;
}
}

return possible_literal_index;
}

/**
* Resolves the clauses `this` and `other`; that is, given:
* this = x1 + x2 + ... + xm + l
* other = y1 + y2 + ... + yn + ~l
*
* then this.resolve(other, l) = x1 + x2 + ... + xm + y1 + y2 + ... + yn
*/
resolve(other, l) {
const literals = [],
polarity = [];

// Take all literals of `this` that are not `l`.
for (let i = 0; i < this.literals.length; i++) {
const literal = this.literals[i];

if (literal !== l) {
literals.push(literal);
polarity.push(this.polarity[i]);
}
}

// Take all literals of `other` that are neither `l` nor in `this`.
for (let i = 0; i < other.literals.length; i++) {
const literal = other.literals[i];

if (literal !== l && !this.literals.includes(literal)) {
literals.push(literal);
polarity.push(other.polarity[i]);
}
}

// Return a new clause that's the disjunction of all these literals.
return new Clause(literals, polarity);
}
}
Insert cell
Insert cell
function preprocess(f) {
if (f.variables !== undefined)
// `f` is already a preprocessed formula.
return f;

// Convert into CNF, in case that wasn't done already.
// For formulas that are already in CNF, this is a noop.
f = cnf(f);

const variables = [],
variables_by_name = {},
clauses = [];

// Transform all clauses into a list of atoms and a list of booleans
// defining the polarity of the clause, i.e. whether it is positive or negative.
for (let i = 0; i < f.clauses.length; i++) {
const input_clause = f.clauses[i],
literals = [],
polarity = [];

for (const literal of input_clause.clauses) {
const positive = typeof literal === 'string',
name = positive ? literal : literal.clause;

let variable;

if (name in variables_by_name) {
variable = variables_by_name[name];
} else {
variable = new Variable(name);
variables_by_name[name] = variable;
variables.push(variable);
}

literals.push(variable);
polarity.push(positive ? 1 : 0);
}

clauses.push(new Clause(literals, polarity));
}

return {
clauses,
variables,
variables_by_name,
};
}
Insert cell
Insert cell
Insert cell
Insert cell
empty_board = {
// Initialize variables.
const value_clauses = [],
line_clauses = [],
column_clauses = [],
subgrid_clauses = [];

// Assign values to each variable.
for (let i = 1; i <= 9; i++)
for (let j = 1; j <= 9; j++) {
const value_clause = [];

for (let k = 1; k <= 9; k++) {
// If `variable` has value `k` (`assignment` is true)...
const assignment = `${i}x${j} = ${k}`;
value_clause.push(assignment);

// ... then other assignments on this line cannot have this value.
for (let i_ = i + 1; i_ <= 9; i_++) {
line_clauses.push(imply(assignment, not(`${i_}x${j} = ${k}`)));
}

// ... then other assignments on this column cannot have this value.
for (let j_ = j + 1; j_ <= 9; j_++) {
column_clauses.push(imply(assignment, not(`${i}x${j_} = ${k}`)));
}

// ... then other assignments in this subgrid cannot have this value.
const start_i = i - (i - 1) % 3,
start_j = j - (j - 1) % 3;

for (let i_ = start_i; i_ < start_i + 3; i_++)
for (let j_ = start_j; j_ < start_j + 3; j_++) {
if (i_ === i && j_ === j)
continue;

subgrid_clauses.push(imply(assignment, not(`${i_}x${j_} = ${k}`)));
}
}

// ... and only one `assignment` can be true.
value_clauses.push(xor(...value_clause));
}

// Aggregate all values and remove duplicates.
const all_clauses = [],
all_clauses_strings = new Set();

for (const clauses of [value_clauses, line_clauses, column_clauses, subgrid_clauses])
for (const clause of clauses) {
// Using JSON for equality is not perfect, but considering how many
// comparisons we'll make it's good to use something reasonably fast
// that preserves equality (although it doesn't account for clauses
// whose literals are equal but in a different order).
const json = JSON.stringify(clause);

if (!all_clauses_strings.has(json)) {
all_clauses.push(clause);
all_clauses_strings.add(json);
}
}

return and(...all_clauses);
}
Insert cell
Insert cell
empty_board_cnf = cnf(empty_board)
Insert cell
Insert cell
Insert cell
example_parsed_sudoku = parse_sudoku(`
5 3 _ _ 7 _ _ _ _
6 _ _ 1 9 5 _ _ _
_ 9 8 _ _ _ _ 6 _

8 _ _ _ 6 _ _ _ 3
4 _ _ 8 _ 3 _ _ 1
7 _ _ _ 2 _ _ _ 6

_ 6 _ _ _ _ 2 8 _
_ _ _ 4 1 9 _ _ 5
_ _ _ _ 8 _ _ 7 9
`)
Insert cell
Insert cell
Insert cell
example_sudoku_grid = make_sudoku_grid(example_parsed_sudoku)
Insert cell
Insert cell
function bcp(f, level) {
for (;;) {
// Find unit clause.
let unit_clause, unit_literal, unit_polarity;

for (const clause of f.clauses) {
const unit_literal_index = clause.find_unique_unassigned_variable();

if (unit_literal_index === Clause.UNSATISFIED)
// The previous iteration led to a clause becoming unsatisfied.
// We return said clause, which means "this clause led to a conflict."
return clause;

if (unit_literal_index >= 0) {
// If the index is positive, we found a unit literal.
unit_clause = clause;
unit_literal = clause.literals[unit_literal_index];
unit_polarity = clause.polarity[unit_literal_index];
break;
}
}

if (unit_clause === undefined)
// No unit clause remains. We return null, which means "there was
// no conflict."
return null;

// Assign value.
unit_literal.assign(unit_polarity, level, unit_clause);
}
}
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
viewof example_with_unit_clause = display(and(or(not('a'), 'b'), 'b', or('a', not('b'), 'c')))
Insert cell
Insert cell
viewof example_without_unit_clause = display_bcp(example_with_unit_clause)
Insert cell
Insert cell
function dpll(f) {
f = preprocess(f);

if (bcp(f) !== null)
// If BCP fails, the formula is unsatisfied.
return null;

// Find all unassigned variables.
const unassigned_variables = f.variables.filter(v => !v.is_assigned);

// If all variables are assigned, we're done.
if (unassigned_variables.length === 0)
return f;

// Otherwise, we pick a `variable`...
const variable = unassigned_variables[0];

// ... and recursively call `dpll` with `variable = 1`...
variable.assign(1);

if (dpll(f) !== null)
return f;

// ... and, if that fails, we restore the starting state...
for (const unassigned_variable of unassigned_variables)
unassigned_variable.unassign();

// ... and we try again with `variable = 0`...
variable.assign(0);

if (dpll(f) !== null)
return f;

// ... and, if that fails yet again, we restore the starting state...
for (const unassigned_variable of unassigned_variables)
unassigned_variable.unassign();

// ... and the formula cannot be satisfied with the current assignments.
return null;
}
Insert cell
Insert cell
dpll(make_sudoku_grid(`
_ _ _ 2 6 _ 7 _ 1
6 8 _ _ 7 _ _ 9 _
1 9 _ _ _ 4 5 _ _

8 2 _ 1 _ _ _ 4 _
_ _ 4 6 _ 2 9 _ _
_ 5 _ _ _ 3 _ 2 8

_ _ 9 3 _ _ _ 7 4
_ 4 _ _ 5 _ _ 3 6
7 _ 3 _ 1 8 _ _ _
`))
Insert cell
Insert cell
async function cdcl(f, decide, pause) {
f = preprocess(f);

// The `decide` and `pause` arguments are optional, but can be changed to
// customize how `cdcl` behaves.
//
// - If `decide` is set, it will be called with a list of unassigned variables,
// and will expect a result { variable: Variable, value: 0 | 1 }.
// This is the function used to pick an assignment to drive the solver.
// By default, it will assign 0 to the first unassigned variable it finds.
// - If `pause` is set, it will be called with the conflicting clause
// every time a conflict is encountered, allowing the caller to display
// some information to the user.
//
// The algorithm could be written without them, but adding them allows us to
// implement two other versions of `cdcl` below, one interactive and one that
// reports on its progress in real time without blocking the browser tab.

// We keep track of the current "decision level," and annote variable assignments
// with that level. This allows us to treat assignments as a graph and to
// non-chronogically backtrack to previous states, i.e. decision levels.
let level = 1;

// Perform unit propagation immediately to reduce the size of the problem.
if (bcp(f, level) !== null)
// Unit propagation failed immediately, which means that the given
// formula was unsatisfiable to start with.
return null;

// While there are variables awaiting assignment...
for (;;) {
// Find all unassigned variables.
const unassigned_variables = f.variables.filter(v => !v.is_assigned);
// If all variables are assigned, we're done.
if (unassigned_variables.length === 0)
return f;

// Otherwise, choose an assignment.
const { variable: variable_to_assign, value: value_to_assign } = decide !== undefined
? await decide(unassigned_variables, f)
: { variable: unassigned_variables[0], value: 1 };

// Enter a new decision level with the given assignment.
level++;
variable_to_assign.assign(value_to_assign, level);

// Given that assignment...
for (;;) {
// ... perform unit propagation ...
const unsatisfied_clause = bcp(f, level);

if (unsatisfied_clause === null) {
// ... and keep going if it succeeded (a return value
// `null` means that no conflict was found).
break;
}

// ... or if there is a conflict, attempt to recover from it.
if (pause !== undefined)
await pause(unsatisfied_clause, f);

if (level === 1)
// If the conflict happens at the first level, though, there's nothing we can do.
return null;

// Learn a new clause that will ensure many of the conflicting
// assignments will not be performed again...
const learnt_clause = learn_from_conflict(unsatisfied_clause, level);

f.clauses.push(learnt_clause);

// ... and backtrack to the asserting level (explained below).
level = compute_asserting_level(learnt_clause, level);

for (const variable of f.variables) {
if (variable.decision_level > level)
variable.unassign();
}
}
}
}
Insert cell
Insert cell
function learn_from_conflict(unsatisfied_clause, conflict_level) {
// Start with the unsatisfied clause.
let learnt_clause = unsatisfied_clause;

for (;;) {
// Find an implied literal assigned at the current decision level in `learnt_clause`.
let literal = null,
assigned_variables = 0;

for (const l of learnt_clause.literals) {
if (l.decision_level !== conflict_level)
// `l` was assigned at a different decision level.
continue;

assigned_variables++;

if (l.antecedent === null)
// `l` is not an implied literal.
continue;

if (literal === null)
literal = l;
}

if (assigned_variables === 1) {
// Unit clause: we can return immediately (using UIP).
return learnt_clause;
}

// Improve our learnt clause by resolving it with the variable's antecedent,
// and continue the process.
learnt_clause = learnt_clause.resolve(literal.antecedent, literal);
}
}
Insert cell
Insert cell
function compute_asserting_level(clause, conflict_level) {
let max_level = 1;

for (const literal of clause.literals) {
const literal_decision_level = literal.decision_level;

if (literal_decision_level !== conflict_level && literal_decision_level > max_level)
max_level = literal_decision_level;
}

return max_level;
}
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
viewof easy_sudoku = solve_sudoku(`
_ _ _ 2 6 _ 7 _ 1
6 8 _ _ 7 _ _ 9 _
1 9 _ _ _ 4 5 _ _

8 2 _ 1 _ _ _ 4 _
_ _ 4 6 _ 2 9 _ _
_ 5 _ _ _ 3 _ 2 8

_ _ 9 3 _ _ _ 7 4
_ 4 _ _ 5 _ _ 3 6
7 _ 3 _ 1 8 _ _ _
`)
Insert cell
viewof wiki_sudoku = solve_sudoku(`
5 3 _ _ 7 _ _ _ _
6 _ _ 1 9 5 _ _ _
_ 9 8 _ _ _ _ 6 _

8 _ _ _ 6 _ _ _ 3
4 _ _ 8 _ 3 _ _ 1
7 _ _ _ 2 _ _ _ 6

_ 6 _ _ _ _ 2 8 _
_ _ _ 4 1 9 _ _ 5
_ _ _ _ 8 _ _ 7 9
`)
Insert cell
viewof hard_sudoku = solve_sudoku(`
_ 2 _ _ _ _ _ _ _
_ _ _ 6 _ _ _ _ 3
_ 7 4 _ 8 _ _ _ _

_ _ _ _ _ 3 _ _ 2
_ 8 _ _ 4 _ _ 1 _
6 _ _ 5 _ _ _ _ _

_ _ _ _ 1 _ 7 8 _
5 _ _ _ _ 9 _ _ _
_ _ _ _ _ _ _ 4 _
`)
Insert cell
Insert cell
miracle_sudoku = {
const _ = 0,
board_clauses = [];

const sudoku = parse_sudoku(`
_ _ _ _ _ _ _ _ _
_ _ _ _ _ _ _ _ _
_ _ _ _ _ _ _ _ _

_ _ _ _ _ _ _ _ _
_ _ 1 _ _ _ _ _ _
_ _ _ _ _ _ 2 _ _

_ _ _ _ _ _ _ _ _
_ _ _ _ _ _ _ _ _
_ _ _ _ _ _ _ _ _
`);

for (let i = 0; i < 9; i++)
for (let j = 0; j < 9; j++) {
if (sudoku[i * 9 + j] !== 0)
board_clauses.push(`${i + 1}x${j + 1} = ${sudoku[i * 9 + j]}`);
}

// The Miracle sudoku has two additional rules that we'll add below.
const rule_clauses = [];

const knights_move_offsets = [[ 2, 1], [ 2, -1], [-2, 1], [-2, -1],
[ 1, 2], [ 1, -2], [-1, 2], [-1, -2]],
kings_move_offsets = [[ 0, 1], [ 0, -1], [ 1, 0], [-1, 0],
[ 1, 1], [ 1, -1], [-1, 1], [-1, -1]],
moves_offsets = knights_move_offsets.concat(kings_move_offsets),
orthogonal_offsets = [[ 1, 1], [ 1, -1], [-1, 1], [-1, -1]];

// Assign values to each variable.
for (let i = 1; i <= 9; i++)
for (let j = 1; j <= 9; j++) {
for (let k = 1; k <= 9; k++) {
// If `variable` has value `k` (`assignment` is true)...
const assignment = `${i}x${j} = ${k}`;

// Any two cells separated by a knight's move or a king's move (in chess)
// cannot contain the same digit.
const moves = [];

for (const [offset_i, offset_j] of moves_offsets) {
let i_ = i + offset_i,
j_ = j + offset_j;

if (i_ >= 1 && i_ <= 9 && j_ >= 1 && j_ <= 9)
moves.push(`${i_}x${j_} = ${k}`);
}

rule_clauses.push(imply(assignment, not(or(...moves))));

// Any two orthogonally adjacent cells cannot contain consecutive digits.
const consecutive_digits = k === 1 ? [2] : k === 9 ? [8] : [k - 1, k + 1];

for (const [offset_i, offset_j] of orthogonal_offsets) {
let i_ = i + offset_i,
j_ = j + offset_j;

if (i_ >= 1 && i_ <= 9 && j_ >= 1 && j_ <= 9) {
for (const consecutive_digit of consecutive_digits)
moves.push(`${i_}x${j_} = ${consecutive_digit}`);
}
}
}
}

return and(...board_clauses, ...rule_clauses, ...empty_board.clauses);
}
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell
Insert cell

Purpose-built for displays of data

Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
Learn more