Skip to content

Abstract rejecting edges

Tereza Schwarzová requested to merge Abstract-rejecting-edges into master

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á

Merge request reports

Loading