Abstract rejecting edges
The qbf formula is created without rejecting SCCs. Those edges are made rejecting after the solving. As a bonus little refactoring was done.
-
removing edges of rejecting SCCs (unoptimized for SCC) -
removing edges of rejecting SCCs (optimized for SCC) -
L1 only unoptimized for SCC
Note: Finding equivalent edges in level 1 is adjusted for SCCs (not for the whole automaton). That means that since we decided to make L1 only for whole automaton (not SCC), it should not be like this. (I changed the L1 so it is just like it is written in the text:
- V e_t -- one edge must be true
- representants for the whole automaton
- L1 only SCC UNOPTIMIZED form
and it seems that for bigger automata it is very slow -- my guess is that it is very hard for the solver to say that the query is UNSAT)
-
September experiments to see which version is the best
Edited by Tereza Schwarzová