- edited description
Pushquantifiers can degrade performance significantly, investigate this!
Issue #518
resolved
!x y: P(x) & Q(y) => R(x,y)
of dus
!x y: ~P(x) | ~Q(y) | R(x,y)
dus mooi clausaal, wordt na push
!x: ~P(x) | (!y: ~Q(y) | R(x,y) )
Waarvoor Tseitins geintroduceerd moeten worden tijdens grounden.
Comments (4)
-
reporter -
Ideetjes:
Misschien moeten we PQ default enkel doen indien er geen context-switch geintroduceerd wordt. (als de totale diepte (alternating conj-disj depth) niet verhoogt, lijkt het een goed idee)
Of... indien de variabelen werkelijk gesplitst worden (als die x niet meer zou voorkomen in de tweede formule (in R dus) zou het ook goed zijn) Dan krijgen we
!x: ~P(x) | T
T <=> !y: ~Q(y) | R(y)
Wat beter is dan het oorpronkeiljke...
-
- changed status to resolved
-
- Log in to comment