Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Divide and Conquer, per-example synthesis #119

Open
THinnerichs opened this issue Oct 3, 2024 · 2 comments
Open

Divide and Conquer, per-example synthesis #119

THinnerichs opened this issue Oct 3, 2024 · 2 comments
Assignees
Labels
enhancement New feature or request

Comments

@THinnerichs
Copy link
Member

THinnerichs commented Oct 3, 2024

Here in HerbSearch: a divide-and-conquer pattern

support two cases:

  • find a solution program for every example (the first one suffices), and combine them into a single program
  • find all solution programs for every example, select the smallest subset, and combine into a single program

The parameters of the procedure:

  • problem: global specification
  • iterator: iterator to run on local specification
  • divide: divides global specification into a collection of local ones
    • takes in a problem
    • output a collection of problems (Vector?)
  • decide: decides whether to keep a program as a solution to a specification/example
    • takes in a problem::AbstractProblem, a program::RuleNode, a mapping from local examples/specification to a set of solutions (discovered so far)
    • returns a Boolean stating whether the program should be kept as a solution to the problem
    • if we only care about finding a single solution (the first one) for an example, then this function should check if we already have it
  • conquer: takes in examples/specification and a corresponding set of solutions, and produces a global program
sub_problems = divide(problem)

#keep track of 
probs_to_sols: Dict{Problem, Vector{RuleNode}} = {}

for prog in iter
    for prob in sb_problems
        keep_program = decide(prob, prog, probs_to_sols)
        
        if keep_program:
               add program to probs_to_sols under prob
    end
end

final_program = conquer(probs_to_sols)

The general loop should be in HerbSearch. (, with default implementations?)
In HerbGarden an example of splitting per-example, and combining as a decision tree (à la EUSolver)

@ReubenJ ReubenJ added the enhancement New feature or request label Oct 3, 2024
@ReubenJ
Copy link
Member

ReubenJ commented Oct 23, 2024

Possible optimization: only run a single iterator to search over programs, the evaluator then calculates the success per-program

@ReubenJ
Copy link
Member

ReubenJ commented Nov 6, 2024

In discussing with @pwochner, we came across a good point to clarify: with this formulation, we're not running many searches per example or group of examples. We're just running one search and deciding whether to keep examples based on which (group of) problem(s) they solve.

Edit: which is exactly what I suggested above. Oops!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants