4 ms·
As an example: Schaefer's dichotomy theorem shows that, when possible, just make sure to use Horn clauses when possible. Takes a bit of thinking but is superi
by nyrikki 3y ago
As an example:
Schaefer's dichotomy theorem shows that, when possible, just make sure to use Horn clauses when possible.
Takes a bit of thinking but is superior to huristics or SAT solvers if you can refactor to allow for it.
- xavxav 3y agoWait, this is very relevant to some work I’ve been doing recently, how do you conclude that Horn clauses should be preferred from Schaefer’s theorem?
- thomasahle 3y agoIsn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.
- Karrot_Kream 3y agoTake a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Schaefer's_dichotomy_theorem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem... (based on Schaefer's "The complexity of satisfiability problems"). Horn clause satisfiability problems (HORN SAT) fall in P-c.
- xavxav 3y agoOh right this is just Horn clauses, not CHCs
- weavermarquez 3y agoNot sure if related, to Schaefer's theorem, but I dove into Answer Set Programming [1] recently, which follows this approach, enabling the use of fast-ish SMT solvers, which are a generalization of SAT solvers! Boolean/Propositional Logic is to Predicate Logic as SAT is to SMT. There's a very nice course about it from the developers of Potassco, one of the best open source Answer Set Programming framework [2]. The syntax looks like Prolog, but predicate negations are a first class citizen, avoids infinite loops. Prolog's approach is like a depth first search through a search tree -- ASP is like a nondeterministic turing machine, exploring all branches simultaneously from the bottom up. [1] https://en.wikipedia.org/wiki/Answer_set_programming https://en.wikipedia.org/wiki/Answer_set_programming [2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfilqPUgpClMKYu https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05DiQfi...