On Fri, 2 Jun 2017 14:56:42 +0000 (UTC) Martin Vaeth <mar...@mvath.de> wrote: > Most examples mentioned earlier were actually 2SAT, i.e., > they are only of the form foo? ( bar ) (possibly with negations) > or can be easily reduced to that. E.g. > ^^ ( foo bar ) > foo? ( !bar graulty bazola ) > can be rewritten as 2 or 3 2SAT-clauses as above, respectively. > > For 2SAT, there are linear time algorithms.
You're getting the encoding wrong. "foo? ( bar )" does not encode as "( !foo \/ bar )", because that would permit the solver to turn on bar even if there is no need to do so. Good luck figuring out how to encode grounding in SAT... -- Ciaran McCreesh
