import { Model, ModelOptions, Literal } from '../../types/index.js';
import { parse } from '../../parser/index.js';
import { astToString } from '../../ast/index.js';
import { clausify } from '../../logic/clausifier.js';
import { groundFormula } from '../../logic/grounding.js';
import { SATEngine } from '../../engines/sat/index.js';
import { parseKey } from '../../engines/sat/serialization.js';
/**
* Find models using SAT solver
*/
export async function findModelsSAT(
premises: string[],
size: number,
opts: ModelOptions,
satEngine: SATEngine
): Promise<Model[]> {
// 1. Ground all premises
const grounded = premises.map(p => {
const ast = parse(p);
return `(${astToString(groundFormula(ast, { domainSize: size }))})`;
}).join(' & ');
// 2. Clausify
const result = clausify(grounded);
if (!result.success || !result.clauses) return [];
const clauses = [...result.clauses];
const models: Model[] = [];
const count = opts.count ?? 1;
// 3. Loop: Solve, Record, Block
while (models.length < count) {
const satResult = await satEngine.checkSat(clauses);
if (!satResult.sat) break;
const model = decodeSATModel(satResult.model!, size);
models.push(model);
// Add blocking clause (negation of current model)
const literals: Literal[] = [];
for (const [key, val] of satResult.model!) {
literals.push({
predicate: key,
args: [],
negated: val // If val=true, NOT key. If val=false, key.
});
}
clauses.push({ literals });
}
return models;
}
/**
* Decode SAT model into Model structure
*/
function decodeSATModel(satModel: Map<string, boolean>, size: number): Model {
const predicates = new Map<string, Set<string>>();
for (const [varName, val] of satModel) {
if (!val) continue;
const parsed = parseKey(varName);
if (parsed) {
const { predicate: pred, args } = parsed;
// Constants like '0', '1' are also returned as true vars in some cases if they are propositions,
// but usually predicates look like p(0,1).
// We should be careful about internal vars generated by clausifier if any.
if (pred.startsWith('$')) continue; // Skip internal vars
if (!predicates.has(pred)) predicates.set(pred, new Set());
predicates.get(pred)!.add(args.join(', '));
}
}
return {
domainSize: size,
domain: Array.from({ length: size }, (_, i) => i),
predicates,
constants: new Map(), // Constants are folded into predicates or grounding
functions: new Map(), // Functions are flattened to predicates
interpretation: ''
};
}
