Answer Set Programming

[philzook58]

An initial answer set programming based extractor. Answer set programming has an intrinsic cycle breaking mechanism, which makes it fairly natural to model the DAG extraction problem. It appears to be slow on the large problems. There is probably still refinement / redundant constraints / symmettry breaking / hints that could speed it up. In addition, giving an upper bound cost from the bottom up method may speed it up.

% we may choose to select this enode if we have selected that class of all it's children.
{ sel(E,I) } :- enode(E,I,_,_), selclass(Ec) : child(E,I,Ec).

% if we select an enode in an eclass, we select that eclass
selclass(E) :- sel(E,_).

% It is inconsistent for a eclass to be a root and not selected.
% This is *not* the same as saying  selclass(E) :- root(E). 
:- root(E), not selclass(E).

% As a redundant constraint, each eclass should have at most one enode selected
:- enode(E,_,_,_), #count { E,I : sel(E,I)} > 1.

% Minimize the sum of costs of all selected enodes.
#minimize { C,E,I : sel(E,I), enode(E,I,_,C) }.

[remysucre]

Nice! In my encoding I had a choice for each leaf to pick or not. Is that a special case of you first rule (since a leaf has no children)?

[philzook58]

Yes, selclass(Ec) : child(E,I,Ec) is an empty forall, which is the same as being true in the case that child(E,I,Ec) is empty.

[mwillsey]

Sorry for the big push. Hopefully the merge isn't too nasty. Lemme know if you have questions / comments on the new data structure and format.

[philzook58]

More details here https://www.philipzucker.com/asp-for-egraph-extraction/

I updated to the new format and added a 15s timeout (after first solution. I haven't figured out how to get clingo's timeout to work yet).

The results so far are not very promising, being utterly dominated in both solve time, stability and solution quality by greedier methods. @remysucre seemed more optimistic, so I'm wondering if perhaps I've missed something or my encoding is worse / putting more work in the solver rather than in the rust.

Adding heuristic lower priority objectives does seem to guide the search process / possibly symmetry break. In particular using the tree cost seems to help, but I have not ported this over to the new version yet.

[remysucre]

@philzook58 sorry that I missed this. This was my first time writing ASP, so you definitely know more than me! It might be worth auto-tuning the different settings for clingo.

[mwillsey]

Closing this as stale for now.