Supercharging Plant Configurations Using Z3

被引：4

作者：

Bjorner, Nikolaj ^{[1
]}

Levatich, Maxwell ^{[2
]}

Lopes, Nuno P. ^{[3
]}

Rybalchenko, Andrey ^{[3
]}

Vuppalapati, Chandrasekar ^{[4
]}

机构：

[1] Microsoft, Redmond, WA 98052 USA

[2] Columbia Univ, New York, NY USA

[3] Microsoft, Cambridge, England

[4] Microsoft, Sunnyvale, CA USA

来源：

INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH | 2021年 / 12735卷

关键词：

SAT; TOOL;

D O I：

10.1007/978-3-030-78230-6_1

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We describe our experiences using Z3 for synthesizing and optimizing next generation plant configurations for a car manufacturing company (The views expressed in this writing are our own. They make no representation on behalf of others). Our approach leverages unique capabilities of Z3: a combination of specialized solvers for finite domain bit-vectors and uninterpreted functions, and a programmable extension that we call constraints as code. To optimize plant configurations using Z3, we identify useful formalisms from Satisfiability Modulo Theories solvers and integrate solving capabilities for the resulting non-trivial optimization problems.

引用

页码：1 / 25

页数：25

共 37 条

[1] Syntax-Guided Synthesis [J].

Alur, Rajeev ;

Bodik, Rastislav ;

Dallal, Eric ;

Fisman, Dana ;

Garg, Pranav ;

Juniwal, Garvit ;

Kress-Gazit, Hadas ;

Madhusudan, P. ;

Martin, Milo M. K. ;

Raghothaman, Mukund ;

Saha, Shamwaditya ;

Seshia, Sanjit A. ;

Singh, Rishabh ;

Solar-Lezama, Armando ;

Torlak, Emina ;

Udupa, Abhishek .

DEPENDABLE SOFTWARE SYSTEMS ENGINEERING, 2015, 40 :1-25

[2] Reveal: A Formal Verification Tool for Verilog Designs [J].

Andraus, Zaher S. ;

Liffiton, Mark H. ;

Sakallah, Karem A. .

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2008, 5330 :343-352

[3]

[Anonymous], 2017, LIPIcs, DOI DOI 10.4230/LIPICS.SNAPL.2017.1

[4]

Barnett M, 2004, LECT NOTES COMPUT SC, V2931, P252

[5]

Belov A., 2012, J SATISF BOOLEAN MOD, V8, P123, DOI [10.3233/SAT190094, DOI 10.3233/SAT190094]

[6]

Berzish M, 2017, PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), P55, DOI 10.23919/FMCAD.2017.8102241

[7]

Biere A., 2020, P SAT COMP 2020 SOLV, VB-2020-1, P51

[8]

Bjorner Nikolaj, 2019, Engineering Trustworthy Software Systems. 4th International School, SETSS 2018. Tutorial Lectures: Lecture Notes in Computer Science (LNCS 11430), P148, DOI 10.1007/978-3-030-17601-3_4

[9] Navigating the Universe of Z3 Theory Solvers [J].

Bjorner, Nikolaj ;

Nachmanson, Lev .

FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2020, 2020, 12475 :8-24

[10]

Bjorner N, 2014, TRACTABILITY, P350

← 1 2 3 4 →