0

Can I define a program synthesis task in Picat, similar to this definition in SyGuS format?

(set-logic LIA)

(synth-fun f ((color Int) (sortAsc Int) (sortDesc Int)) Int 
  ((I Int) (B Bool))
  ((I Int (color sortAsc sortDesc 0 1 2 3 4
           (ite B I I)))
   (B Bool ((<= I I) (= I I))))
)

(declare-var color Int)
(declare-var sortAsc Int)
(declare-var sortDesc Int)

(constraint (= (f 1 2 2) 0))
(constraint (= (f 1 4 0) 2))
(constraint (= (f 1 1 3) 0))
(constraint (= (f 1 3 1) 0))
(constraint (= (f 1 0 4) 3))

(constraint (= (f 1 2 1) 0))
(constraint (= (f 1 0 3) 3))
(constraint (= (f 1 3 0) 2))
(constraint (= (f 1 1 2) 0))

(check-synth)
Paul Jurczak
  • 7,008
  • 3
  • 47
  • 72

1 Answers1

1

Picat does not have any built-in support for program synthesis. It has support of constraint modelling using Constraint Logic Programming (CLP) with support for CP/SAT/MIP/SMT solvers, but the SMT solver is used as a constraint solver.

Perhaps related: I wrote an (experimental) symbolic regression program which might be used for similar tasks: http://hakank.org/picat/symbolic_regression.pi

Admittedly, I'm not sure exactly what operators are allowed in the presented SyGuS program, but given the data in the "constraints" section and with some given operators (if_then_else and if_less) and some constants (0..3), it finds some possible solutions such as the following for the input [1,2,3] (as [A,B,C]):

 if_less(0,B * C,0,if_less(B,A,3,2)) 
 if_less(0,C,if_less(B,A,3,0),2)

as well as a more complex variants, all giving 0 as the output.

The data file shows some of the different solutions from a single run of the program: http://hakank.org/picat/symbolic_regression_program_synthesis.pi

Note that the program is not deterministic and will yield different solutions each time it's run, though smaller solutions tends be selected more often.

Also, the solutions might not be proper Picat syntax, so one have to translate it to proper syntax. For example, the first solution if_less(0,B * C,0,if_less(B,A,3,2)) corresponds to this Picat program/snippet

if 0 < B * C then
   println(0)
elseif B < A then
   println(3)
else
   println(2)
end,

or - better - using cond/3:

cond(0 < B * C, 0, cond(B < A, 3, 2))

The program is tested in the test predicate of symbolic_regression_program_synthesis.pi And it generates all the expected outputs from the data:

[input = [1,2,2],expected = 0,out = 0,verdict = ok]
[input = [1,4,0],expected = 2,out = 2,verdict = ok]
[input = [1,1,3],expected = 0,out = 0,verdict = ok]
[input = [1,3,1],expected = 0,out = 0,verdict = ok]
[input = [1,0,4],expected = 3,out = 3,verdict = ok]
[input = [1,2,1],expected = 0,out = 0,verdict = ok]
[input = [1,0,3],expected = 3,out = 3,verdict = ok]
[input = [1,3,0],expected = 2,out = 2,verdict = ok]
[input = [1,1,2],expected = 0,out = 0,verdict = ok]

At my Picat page (http://hakank.org/picat/) there are quite a few other examples of using this (search for "symbolic regression"). I also wrote a short introduction of the program in the Picat group: https://groups.google.com/g/picat-lang/c/1CngmWD0_tw/m/m_9T_SViEAAJ

hakank
  • 6,629
  • 1
  • 17
  • 27
  • 1
    Thank you for a detailed answer. Operations allowed in my examples are *if-then-else* and *<=*. *==* is not needed. cvc5 produces *(define-fun f ((x Int) (y Int)) Int (ite (<= 5 x) 9 x))* result. I have not used Picat yet. Does your function generator try all syntactically valid combinations of *Ops = [if_less,if_then_else], Constants = 0..3, Vars = ['A','B','C']*? – Paul Jurczak Jun 28 '23 at 05:19
  • 1
    The program symbolic_regression.pi uses the ideas of genetic programming, i.e. it picks operators and values randomly (based on the GP approach); thus it does not test all valid combinations. I wrote another Picat program (http://hakank.org/picat/symbolic_function_induction.pi ) which do a systematic search, but it's limited and blows up quite fast, such as for your problem. – hakank Jun 28 '23 at 06:26
  • Do you think Picat offers a substantial advantage vs. Python packages, e.g. PonyGE2 https://github.com/PonyGE/PonyGE2 or another one manipulating Python ASTs? – Paul Jurczak Jun 29 '23 at 02:05
  • 1
    @PaulJurczak Well, it depends. Picat has much of the advantages of Prolog (support for logic programming, nondeterministic predicates, DCGs as well as support for constraint modeling) which can be an advantage for this. However, it does not directly support meta-interpreters as well as Prolog do which might be harder than using Python's libraries. – hakank Jun 29 '23 at 08:50