search

princeton-vl / MetaQNL

Learning Symbolic Rules for Reasoning in Quasi-Natural Language: https://arxiv.org/abs/2111.12038
BSD 2-Clause "Simplified" License
7 stars 0 forks source link

Encoding proof constraints in MetaQNL that don't follow CNF format #22

Closed realharryhero closed 3 months ago

realharryhero commented 3 months ago

Sorry for the many questions. When encoding the optimization problem with a MaxSAT problem, there's a constraint of the form $(\text{cr}_1 \land \text{cr}_2) \lor \text{cr}_3 \lor (\text{cr}_4 \land \text{cr}_5).$ But constraints according to the normal form take the form of $r_1 \lor r_2 \lor \cdots \lor r_n$ (with negations ($\neg$) in each of the rules as well); moreover it shouldn't be possible (or not that easy) to have a constraint with logical ands in it.

Perhaps a constraint such as $$r_1 \land r_2 \land \cdots \land rn = \bigwedge{k = 1}^n rk$$ with weight $w$ was created was by making a constraint of the form $$\neg \left(\bigwedge{k = 1}^n rk\right) = \left(\bigvee{k = 1}^n \neg r_k\right)$$ with weight $-w.$ But then at least one of $w$ or $-w$ will have to be negative, and then there will be a constraint with a negative weight, which is not normally allowed.

Perhaps this was done by making a new variable $r_k' = \neg r_k$ for all such $r_k,$ and rewriting the constraints with those new $r_k'.$ Was it done this way, or through some other way? Thank you!

(I've found a theoretical solution, by encoding the the constraint $$\left(\bigvee_{k = 1}^n \neg rk\right)$$ as $$C = \neg \left(\bigwedge{k = 1}^n r_k\right),$$ and then converting this to CNF form by doing a MinSAT algorithm $\neg C$ via a MaxSAT algorithm for $C,$ as per this post. It is rather complicated, though, and blows up the number of constraints by k times - there should be a faster way.)

yangky11 commented 3 months ago

I'm not sure if I understand the question. Why is it impossible to have constraints with logical AND?

For your reference, here is ho constraint encoding is implemented: https://github.com/princeton-vl/MetaQNL/blob/3e30483ee22c5d1af8cf92bc3ba0a99627e6a5e8/src/optimization/metainduce_trainer.jl#L294

realharryhero commented 3 months ago

It is possible, but not with Max-SAT solvers. Z3 is an SMT solver; i.e. the clauses need not be a constraint only with ORs, as in SAT solvers; the clauses can include anything, including logical ANDs or generally any kind of first-order expression. Thank you!

yangky11 commented 3 months ago

That's just a matter or preprocessing, e.g., you can look into how the code supports OpenWBO: https://github.com/princeton-vl/MetaQNL/blob/main/src/optimization/maxsat_solvers.jl