Распараллеливание рекурсивных вычислений ветвления в scala с использованием фьючерсов

Question

Я пытаюсь распараллелить SAT-решатель в Scala с использованием фьючерсов.

Алгоритм решения задачи SAT неплотно типа (псевдо-код):

def has_solution(x): 
    if x is a solution: 
     return true 
    else if x is not a solution: 
     return false 
    else: 
     x1 = left_branch(x) 
     x2 = right_branch(x) 
     return has_solution(x1) or has_solution(x2) 

Так я вижу возможность распараллеливания вычислений, когда я ветвление проблемы.

Как я могу это сделать с помощью фьючерсов? Мне нужно ждать результатов от has_solution (x1) и has_solution (х2), а также:

1. возвращающие как только либо ветвь возвращает истину
2. Возврат ложно, если обе ветви возвращают ложные

Мой текущий подход заключается в следующем:

object DPLL { 
    def apply(formula: Formula): Future[Boolean] = { 
    var tmp = formula 

    if (tmp.isEmpty) { 
     Future { true } 
    } else if (tmp.hasEmptyClause) { 
     Future { false } 
    } else { 

     for (unitClause <- tmp.unitClauses) tmp = tmp.propagateUnit(unitClause); 
     for (pureLiteral <- tmp.pureLiterals) tmp = tmp.assign(pureLiteral); 

     if (tmp.isEmpty()) 
     Future { true } 
     else if (tmp.hasEmptyClause) 
     Future { false } 
     else { 
     val nextLiteral = tmp.chooseLiteral 

Вот где ветвление происходит и где я хотел бы ждать вычислений, как описано выше:

 for (f1 <- DPLL(tmp.assign(nextLiteral)); 
      f2 <- DPLL(tmp.assign(-nextLiteral))) 
      yield (f1 || f2) 
     } 
    } 
    } 
} 

Это выглядит неправильно, когда я запускаю его, потому что я никогда не смогу полностью использовать свои сердечники (8).

У меня есть интуиция Я не должен использовать фьючерсы для такого рода вычислений. Возможно, фьючерсы подходят только для асинхронных вычислений. Должен ли я попробовать какой-то более низкий уровень потокового или актерского подхода для этого? Благодарю.

Answer 1

Этот код работает последовательно из-за блока! Вычисление f2 начинается после завершения вычисления f1.

for { 
    f1 <- DPLL(tmp.assign(nextLiteral)) 
    f2 <- DPLL(tmp.assign(-nextLiteral)) 
} yield f1 || f2 

Над блока приводит к следующим flatMap/map последовательности и что flatMap/map делает, чтобы запустить функцию после того, как значение присутствует.

DPLL(tmp.assign(nextLiteral)).flatMap(f1 => 
    DPLL(tmp.assign(-nextLiteral)).map(f2 => 
    f1 || f2) 

Один простой трюк для запуска вычислений параллельно, назначая их значения и доступа к этому значению в для понимания

val comp1 = DPLL(tmp.assign(nextLiteral)) 
val comp2 = DPLL(tmp.assign(-nextLiteral)) 
for { 
    f1 <- comp1 
    f2 <- comp1 
} yield f1 || f2