给定一个图，若干条Horn-SAT约束以及一个点 $s$，求是否存在一条不经过重复节点的路径从 $s$ 开始，使得其通过的点满足Horn-SAT约束。

例：在图$[(1,2),(2,3),(1,4)]$,$s=1$ 的情况下满足(3 | !2) & (4 | !3 | !2)的合法路径存在(1->4)。

请问有多项式复杂度的做法吗？