Accelerating LTL satisfiability checking by SAT solvers

2018 ◽  
Vol 28 (6) ◽  
pp. 1011-1030
Author(s):  
Jianwen Li ◽  
Geguang Pu ◽  
Lijun Zhang ◽  
Moshe Y Vardi ◽  
Jifeng He
Keyword(s):  
Sat Solvers ◽  
Satisfiability Checking ◽  
Ltl Satisfiability Checking

scholarly journals Constraint LTL satisfiability checking without automata

2014 ◽  
Vol 12 (4) ◽  
pp. 522-557 ◽  
Author(s):  
Marcello M. Bersani ◽  
Achille Frigeri ◽  
Angelo Morzenti ◽  
Matteo Pradella ◽  
Matteo Rossi ◽  
...  
Keyword(s):  
Satisfiability Checking ◽  
Ltl Satisfiability Checking

scholarly journals SAT-Based Explicit LTLf Satisfiability Checking

2019 ◽  
Vol 33 ◽  
pp. 2946-2953 ◽  
Author(s):  
Jianwen Li ◽  
Kristin Y. Rozier ◽  
Geguang Pu ◽  
Yueling Zhang ◽  
Moshe Y. Vardi
Keyword(s):  
Temporal Logic ◽  
Transition System ◽  
Search Problem ◽  
Sat Solving ◽  
Second Best ◽  
Sat Solvers ◽  
Path Search ◽  
Speed Up ◽  
Satisfiability Checking ◽  
Novel Algorithm

We present a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTLf satisfiability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver.

An explicit transition system construction approach to LTL satisfiability checking

2017 ◽  
Vol 30 (2) ◽  
pp. 193-217 ◽  
Author(s):  
Jianwen Li ◽  
Lijun Zhang ◽  
Shufang Zhu ◽  
Geguang Pu ◽  
Moshe Y. Vardi ◽  
...  
Keyword(s):  
Transition System ◽  
System Construction ◽  
Satisfiability Checking ◽  
Ltl Satisfiability Checking

Masking Circuit Faults and Trojan Circuit Injections Using Sat Solvers

2021 ◽  
Vol 63 (12) ◽  
pp. 2178-2188
Author(s):  
A. Yu. Маtrosova ◽  
V. А. Provkin ◽  
V. Z. Tychinskiy ◽  
Е. А. Nikolaeva ◽  
G. G. Goshin
Keyword(s):  
Sat Solvers
Sign in / Sign up

Export Citation Format

Share Document