Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Do we need a smarter SAT solver? #199

Open
yhx-12243 opened this issue Nov 29, 2024 · 2 comments
Open

feat: Do we need a smarter SAT solver? #199

yhx-12243 opened this issue Nov 29, 2024 · 2 comments

Comments

@yhx-12243
Copy link
Contributor

yhx-12243 commented Nov 29, 2024

In my opinion, it is not necessary now but this can be proposed first maybe we can used one day.

Nowadays pi-base use a very simple deduction logic and as we can see, the deduction is actually a SAT-problem which can be manipulated with SAT solvers.

private apply(
implication: Theorem,
): Contradiction<TheoremId, PropertyId> | undefined {
const a = implication.when
const c = implication.then
const av = evaluate(a, this.traits)
const cv = evaluate(c, this.traits)
if (av === true && cv === false) {
return this.contradiction(implication.id, [
...properties(a),
...properties(c),
])
} else if (av === true) {
return this.force(implication.id, c, [...properties(a)])
} else if (cv === false) {
return this.force(implication.id, negate(a), [...properties(c)])
}
}

For example, it can be deduced P is false if I set following artificially:
101
102
103
104

@StevenClontz
Copy link
Member

@jamesdabbs is much more familiar with the deduction engine, so I'll let him comment

@danflapjax
Copy link
Collaborator

As far as I'm aware, it just uses boolean constraint propagation at the moment. I've been interested in improving it and have done some reading on algorithms, but I haven't found the time to actually write much code recently.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants