Constraint Solving

import { ConstraintBuilder, allDifferent, createNeuroSymbolic, isZ3Available, solveSAT } from '@cogitator-ai/neuro-symbolic';

const schedule = ConstraintBuilder.create('meeting-rooms');
const engineering = schedule.int('engineering', 0, 3);
const product = schedule.int('product', 0, 3);
const design = schedule.int('design', 0, 3);
const marketing = schedule.int('marketing', 0, 3);

schedule.assert(allDifferent(engineering, product, design, marketing), 'one team per slot');
schedule.assert(engineering.lt(product), 'engineering before product');
schedule.assert(design.neq(0), 'design not in the first slot');
schedule.assert(marketing.gt(engineering), 'marketing after engineering');

const slots = ['9:00', '10:00', '11:00', '13:00'];
const solved = solveSAT(schedule.build(), { timeout: 5000, maxIterations: 5000 });
if (solved.status === 'sat' && solved.model) {
  for (const [team, slot] of Object.entries(solved.model.assignments)) {
    console.log(`${slots[slot as number]} ${team}`);
  }
}

const ns = createNeuroSymbolic();
const staffing = ns.createConstraintProblem('staffing');
const seniors = staffing.int('seniors', 0, 10);
const juniors = staffing.int('juniors', 0, 10);
staffing.assert(seniors.add(juniors).gte(8), 'cover 8 shifts');
staffing.assert(seniors.mul(2).gte(juniors), 'one senior per two juniors');
staffing.minimize(seniors.mul(300).add(juniors.mul(180)));

const optimal = await ns.solve(staffing.build());
console.log(`solver: ${(await isZ3Available()) ? 'Z3' : 'built-in'}`);
if (optimal.data?.status === 'sat') {
  const { assignments, objectiveValue } = optimal.data.model;
  console.log(`hire ${assignments.seniors} seniors and ${assignments.juniors} juniors, cost ${objectiveValue}`);
}

pnpm add @cogitator-ai/neuro-symbolic

npx tsx constraint-solving.ts

npx tsx examples/advanced/02-neuro-symbolic.ts