Functional synthesis via input–output separation
Tóm tắt
Boolean functional synthesis is the process of constructing a Boolean function from a Boolean specification that relates input and output variables. Despite recent developments in synthesis algorithms, Boolean functional synthesis remains a challenging problem even when state-of-the-art techniques are used for decomposing the specification. In this work, we present a new decomposition approach that decomposes the specification into separate input and output components. To begin with, we adapt the notion of “sequential decomposition” and present a framework that allows the input and output components to be independently synthesized and then re-composed to yield an implementation of the overall specification. Although theoretically appealing, this approach suffers from some practical drawbacks, as evidenced by our experiments. This motivates us to propose a relaxed approach to synthesis by decomposition. In the relaxed approach, we start with a specification given as a conjunctive normal form (CNF) formula, and obtain a decomposition of the specification by alternatingly analyzing the input and output components repeatedly. We also exploit specific properties of these components to ultimately implement the overall specification. We prove that if the input component of the CNF specification has specific structural properties, our approach can achieve synthesis in polynomial time. We also show by experimental evaluations that our algorithm performs well in practice on instances that are challenging for existing state-of-the-art tools. Thus, our decomposition-based synthesis approach serves as a good complement to other state-of-the-art techniques in a portfolio approach to Boolean functional synthesis.
Tài liệu tham khảo
Akshay S, Arora J, Chakraborty S, Krishna S, Raghunathan D, Shah S (2019) Knowledge compilation for Boolean functional synthesis. In: Formal methods in computer-aided design, FMCAD 2019, pp 161–169
Akshay S, Chakraborty S, Goel S, Kulal S, Shah S (2018) What’s hard about Boolean functional synthesis? In: Computer aided verification–30th international conference, CAV 2018, pp 251–269. https://doi.org/10.1007/978-3-319-96145-3_14
Akshay S, Chakraborty S, John AK, Shah S (2017) Towards parallel Boolean functional synthesis. In: Tools and algorithms for the construction and analysis of systems–23rd international conference, TACAS 2017, pp 337–353. https://doi.org/10.1007/978-3-662-54577-5_19
Alur R, Madhusudan P, Nam W (2005) Symbolic computational techniques for solving games. STTT 7(2):118–128
Ansótegui C, Bonet ML, Levy J (2009) Solving (Weighted) partial MaxSAT through satisfiability testing. In: Theory and applications of satisfiability testing–SAT 2009–12th international conference, pp 427–440. https://doi.org/10.1007/978-3-642-02777-2_39
Audemard G, Simon L (2009) Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of the 21st international joint conference on artificial intelligence, IJCAI 2009, pp 399–404. http://ijcai.org/Proceedings/09/Papers/074.pdf
Bacchus F, Järvisalo M, Malik S (2021) Maxium satisfiability. In: Handbook of satisfiability, pp 929–991
Balabanov V, Jiang JHR (2012) Unified QBF certification and its applications. Form Methods Syst Des 41(1):45–65. https://doi.org/10.1007/s10703-012-0152-6
Balabanov V, Jiang JR (2011) Resolution proofs and Skolem functions in QBF evaluation and applications. In: Computer aided verification–23rd international conference, CAV 2011, pp 149–164. https://doi.org/10.1007/978-3-642-22110-1_12
Balabanov V, Widl M, Jiang JR (2014) QBF Resolution systems and their proof complexities. In: Theory and applications of satisfiability testing–SAT 2014–17th international conference, pp 154–169. https://doi.org/10.1007/978-3-319-09284-3_12
Boole G (1847) The mathematical analysis of logic. Philosophical Library, New York
Bryant RE (1986) Graph-based algorithms for Boolean function manipulation. IEEE Tran Comput 35(8):677–691. https://doi.org/10.1109/TC.1986.1676819
Chakraborty S, Fried D, Tabajara LM, Vardi MY (2018) Functional synthesis via input-output separation. In: Bjørner N, Gurfinkel A (eds) Formal methods in computer aided design FMCAD 2018. IEEE, New York
Eén N, Sörensson N (2003) An extensible SAT-solver. In: Theory and applications of satisfiability testing–SAT 2003–6th International Conference, pp 502–518. https://doi.org/10.1007/978-3-540-24605-3_37
Fried D, Legay A, Ouaknine J, Vardi MY (2018) Sequential relational decomposition. In: Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, pp. 432–441. https://doi.org/10.1145/3209108.3209203. http://doi.acm.org/10.1145/3209108.3209203
Fried D, Tabajara LM, Vardi MY (2016) BDD-Based Boolean functional synthesis. In: Computer aided verification–28th international conference, CAV 2016, pp 402–421. https://doi.org/10.1007/978-3-319-41540-6_22. http://dx.doi.org/10.1007/978-3-319-41540-6_22
Ganian R, Szeider S (2017) New width parameters for model counting. In: Theory and applications of satisfiability testing–sat 2017–20th international conference, pp 38–52. https://doi.org/10.1007/978-3-319-66263-3_3
Golia P, Roy S, Meel KS (2020) Manthan: a data driven approach for Boolean function synthesis. https://arxiv.org/abs/2005.06922
Heule M, Seidl M, Biere A (2014) Efficient extraction of skolem functions from QRAT proofs. In: Formal methods in computer-aided design, FMCAD 2014, pp 107–114. https://doi.org/10.1109/FMCAD.2014.6987602
Ignatiev A, Morgado A, Planes J, Marques-Silva J (2013) Maximal falsifiability–definitions, algorithms, and applications. In: Logic for programming, artificial intelligence, and reasoning–19th international conference, LPAR-19, pp 439–456. https://doi.org/10.1007/978-3-642-45221-5_30
Jacobs S, Bloem R, Brenguier R, Könighofer R, Pérez GA, Raskin J, Ryzhyk L, Sankur O, Seidl M, Tentrup L, Walker A (2015) The second reactive synthesis competition (SYNTCOMP 2015). In: Proceedings fourth workshop on synthesis, SYNT 2015, pp 27–57
Jiang JR (2009) Quantifier elimination via functional composition. In: Computer aided verification, 21st international conference, CAV 2009, pp 383–397. https://doi.org/10.1007/978-3-642-02658-4_30
Jo S, Matsumoto T, Fujita M (2012) SAT-based automatic rectification and debugging of combinational circuits with LUT insertions. In: Proceedings of the 2012 IEEE 21st Asian test symposium, ATS ’12, pp 19–24. IEEE Computer Society
John AK, Shah S, Chakraborty S, Trivedi A, Akshay S (2015) Skolem functions for factored formulas. In: Formal methods in computer-aided design, FMCAD 2015, pp 73–80
Kuehlmann A, Paruthi V, Krohm F, Ganai M (2002) Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans Comput Aided Des Integr Circuits Syst 21(12):1377–1394. https://doi.org/10.1109/TCAD.2002.804386
Kukula JH, Shiple TR (2000) Building circuits from relations. In: Computer aided verification, 12th international conference, CAV 2000, pp 113–123. https://doi.org/10.1007/10722167_12
Lakkaraju H, Bach SH, Jure L (2016) Interpretable decision sets: a joint framework for description and prediction. In: International conference on knowledge discovery and data mining (KDD), pp 1675V–1684
Li CM, Manyà F (2009) MaxSAT, hard and soft constraints. In: Handbook of satisfiability, pp 613–631. https://doi.org/10.3233/978-1-58603-929-5-613
Lowenheim L (1910) Über die Auflösung von Gleichungen in Logischen Gebietkalkul. Math Ann 68:169–207
Macii E, Odasso G, Poncino M (2006) Comparing different Boolean unification algorithms. In: Proceedings of 32nd Asilomar conference on signals, systems and computers, pp 17–29
Martins R, Manquinho VM, Lynce I (2014) Open-WBO: a modular MaxSAT solver. In: Theory and applications of satisfiability testing–SAT 2014–17th international conference, pp 438–445. https://doi.org/10.1007/978-3-319-09284-3_33
Narizzano M, Pulina L, Tacchella A (2006) The QBFEVAL web portal. In: Logics in artificial intelligence, pp 494–497. Springer, Berlin
Niemetz A, Preiner M, Lonsing F, Seidl M, Bierre A (2012) Resolution-based certificate extraction for QBF - (tool presentation). In: Theory and applications of satisfiability testing–SAT 2012–15th international conference, pp 430–435
Rabe MN, Seshia SA (2016) Incremental determinization. In: Theory and applications of satisfiability testing–SAT 2016–19th International Conference, pp 375–392. https://doi.org/10.1007/978-3-319-40970-2_23
Rabe MN, Tentrup L (2015) CAQE: A certifying QBF solver. In: Formal methods in computer-aided design, FMCAD 2015, pp 136–143
Rivest RL (1987) Learning decision lists. Mach Learn 2(3):229–246. https://doi.org/10.1007/BF00058680
Silva JPM, Lynce I, Malik S (2009) Conflict-driven clause learning SAT solvers. In: Handbook of satisfiability, pp 131–153. https://doi.org/10.3233/978-1-58603-929-5-131
Solar-Lezama A (2013) Program sketching. STTT 15(5–6):475–495
Solar-Lezama A, Rabbah RM, Bodík R, Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: Proceedings of the ACM SIGPLAN 2005 conference on programming language design and implementation, pp 281–294
Srivastava S, Gulwani S, Foster JS (2013) Template-based program verification and program synthesis. STTT 15(5–6):497–518
Stockmeyer LJ (1976) The polynomial-time hierarchy. Theort Comput Sci 3(1):1–22
Tabajara LM (2018) BDD-based Boolean synthesis. Master’s thesis, Rice University
Tabajara LM, Vardi MY (2017) Factored Boolean functional synthesis. In: Formal methods in computer aided design, FMCAD 2017, pp 124–131. https://doi.org/10.23919/FMCAD.2017.8102250
Zhu, S., Tabajara LM, Li J, Pu G, Vardi, MY (2017) Symbolic LTLf synthesis. In: Proceedings of the 26th international joint conference on artificial intelligence, IJCAI 2017, pp 1362–1369 . https://doi.org/10.24963/ijcai.2017/189