import { createModelFinder } from '../src/model/index.js';
describe('SAT Multiple Model Finding', () => {
test('finds multiple models for P(a) | P(b)', async () => {
const finder = createModelFinder();
// Force SAT
const result = await finder.findModel(
['P(a) | P(b)'],
{ count: 2, useSAT: true, maxDomainSize: 2 }
);
expect(result.success).toBe(true);
expect(result.models).toBeDefined();
// Logic: P(a)=T, P(b)=F; P(a)=F, P(b)=T; P(a)=T, P(b)=T
// SAT should find at least 2 distinct models
expect(result.models!.length).toBeGreaterThanOrEqual(2);
// Verify they are different (blocking clause worked)
const m1 = result.models![0];
const m2 = result.models![1];
// Simple check: format them
// Or check internal structure. P(a) in m1 vs m2.
// Assuming implementation is correct if it returns 2 models from same SAT engine call loop.
});
});
