Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 02:20 - 02:40 at Koala - Formal Methods (1) Chair(s): Nazareno Aguirre

The All-SAT (All-SATisfiable) problem focuses on finding all satisfiable assignments of a given propositional formula, whose applications include model checking, automata construction, and logic minimization. A typical ALL-SAT solver is normally based on iteratively computing satisfiable assignments of the given formula. In this work, we introduce BASolver, a backbone-based All-SAT solver for propositional formulas. Compared to the existing approaches, BASolver generates shorter blocking clauses by removing backbone variables from the partial assignments and the blocking clauses. We compare BASolver with 4 existing ALL-SAT solvers, namely MBlocking, BC, BDD, and NBC. Experimental results indicate that although finding all the backbone variables consumes additional computing time, BAsolver is still more efficient than the existing solvers because of the shorter blocking clauses and the backbone variables used in it.

With the 608 formulas, BASolver solves the largest amount of formulas (86), which is 22%, 36%, 68%, 86% more formulas than MBlocking, BC, NBC, and BDD respectively. For the formulas that are both solved by BASolver and the other solvers, BASolver uses 88.4% less computing time on average than the other solvers. For the 215 formulas which first 1000 satisfiable assignments are found by at least one of the solvers, BASolver uses 180% less computing time on average than the other solvers.

Tue 22 Sep
Times are displayed in time zone: (UTC) Coordinated Universal Time change

02:20 - 03:20
Formal Methods (1)NIER track / Research Papers at Koala
Chair(s): Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto
Accelerating All-SAT Computation with Short Blocking Clauses
Research Papers
Yueling ZhangSingapore Management University, Geguang PuEast China Normal University, Jun SunSingapore Management University
A Predictive Analysis for Detecting Deadlock in MPI Programs
Research Papers
Yu HuangSouthwestern University of Finance and Economics, Benjamin OglesBrigham Young University, Eric MercerBrigham Young University
Proving Termination by k-Induction
NIER track
Jianhui ChenTsinghua University, Fei HeTsinghua University, China