BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:7883d266-5dfa-45a3-8808-8513003e8cf5
X-WR-CALNAME:[MTV/SYNTHESE] Suptratik Chakraborty (IIT Bombay) - On Tractab
 le Representations for Boolean Functional Synthesis
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20270328T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20251026T030000
RDATE:20261025T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20250330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:7883d266-5dfa-45a3-8808-8513003e8cf5
DTSTAMP:20260411T104053Z
CLASS:PUBLIC
DESCRIPTION:Given a relational specification \varphi(X\, Y_1\, ... Y_n)\, B
 oolean functional synthesis concerns the construction of Boolean functions
  F_1(X)\,  ... F_n(X)  such that \varphi(X\, F_1\, ... F_n) is semanticall
 y equivalent to \exists Y_1\, ... Y_n \varphi(X\, Y_1\, ... Y_n).   Such f
 unctions are also called Skolem functions\, and their algorithmic synthesi
 s has many applications\, including in program synthesis\, QBF-SAT certifi
 cate generation\, circuit repair\,  reactive synthesis\, planning and the 
 like.  The synthesis problem is intractable unless long-standing complexit
 y-theoretic conjectures are falsified.  Fortunately\, polynomial-time synt
 hesis algorithms can be designed if \varphi is represented in special norm
 al forms.  In this talk\, we present some such normal forms\, including th
 ose that were originally studied in AI and formal verification\, and  othe
 rs like Synthesis Negation Normal Form (SynNNF) and Subset And-Unrealizabl
 e Normal Form (SAUNF) that have arisen from our study of synthesis. We dis
 cuss properties of such forms and relations between them\, and show that e
 very universal representation that admits polynomial-time synthesis is pol
 ynomially reducible to SAUNF.   We also sketch the idea behind compilation
  algorithms that convert a Boolean specification given as a circuit to Syn
 NNF or SAUNF.  We conclude with empirical evidence that shows that such co
 mpilation algorithms hold promise in practice.\n\n\nImport automatique dep
 uis https://framagenda.org/remote.php/dav/public-calendars/D3yqF7nwys9amfy
 Y?export par sync_icals_to_drupal.py pour M2F
DTSTART;TZID=Europe/Paris:20250612T130000
DTEND;TZID=Europe/Paris:20250612T140000
LOCATION:LaBRI\, 178
SEQUENCE:0
SUMMARY:[MTV/SYNTHESE] Suptratik Chakraborty (IIT Bombay) - On Tractable Re
 presentations for Boolean Functional Synthesis
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
