일찍이 나온 branching heuristics 인 Bohm's Heuristic, Maximum Occurrences on Minimum sized clauses(MOM), Jeroslow-Wang 알고리즘들은 욕심 많은 알고리즘으로, 가장 많은 clause에 포함되어 있거나 또는, 가장많은 수의 implication을 가지고 있는 변수를 선택하였다.
이러한 heuristic 들은 각각의 free 변수들의 branching 효과를 평가하기 위한 function으로 사용 되며, 가장 높은 값을 갖는 변수를 선택하게 된다. 대부분의 function들이 clause의 길이 정보 같은 clause database 의 통계에 기반으로 하고 있으므로 '신뢰적이다' 라고 할 수 있지만,
이러한 통계를 기초로한 방법들은 random 한 SAT instance(풀기 어려운 수학적 난제) 에는 유용할지라도 대개는 구조적문제(실세계의 문제)에 대한 관련된 정보들을 얻어내지 못한다.

“The Impact of Branching Heuristics in Propositional Satisfiability Algorithms” 논문의 저자인 Marques-Silva는 literal count heuristic 의 사용을 제안했다.
literal count heuristic은 각 단계에서의 나타나는 주어진 변수들중에 풀리지 않은(Unresolved) 변수의 수를 count 한다. 특히, Marques-Silva는 양의 리터럴과 음의 리터럴의 값의 합이 가장 큰 변수를 선택하는 heuristic이 보다 좋은 결과를 나타낸다는것을 실험을 통해 발견했다.
인지할 점은 어떤 면에 있어, 다른 변수는 다른 count 값을 할당할 것이라는 점에서 count들은 상황 종속적이라는 것이다.(매 단계 즉, 그 상황마다 count 값이 달라지기 때문에)
이유는 하나의 clause는 풀리지 않았거나(unresolved) 현재 변수할당에 의존하기 때문이다.
상황 종속적인 이유로 인해 count는 매 순간 decide_next_branch()가 호출될 때 마다, 모든 free variable들이 매번 다시 계산되어야 할 필요가 있다.

solver들이 보다 효율적으로 구현되는 만큼 branching을 위한 count의 계산은 실행시간을 지배한다(점유한다). 그러므로, 보다 효율적이고 효과적인 branching heuristic들이 필요하다.

VSIDS(또 다른 branching heuristic, 이 논문에서 사용하는 알고리즘)
- 각각의 literal이 score를 갖는다
- 최초, score는 처음 문제(initial problem)에서 발견된 literal의 수이다. 
- conflict 발생으로 인해 새로이 생성되는 clause가 clause DB에 들어오면 clause에 포함된
variable들의 값을 증가시켜준다.
- 주기적으로, 모든 variable들의 score를 constant 값으로 나눈다.
- 가장 높은 scroe를 유지하고 있는 unresolved variable을 선택한다.(우선순위 Queue 와 같은 자료구조를 사용..)
이 알고리즘은 low overhead 이다. 왜냐하면 conflict이 발생했을 때 variable의 score를 update 해주기 때문이다. VSIDS는 다른 Branching Heuristic 알고리즘들과 비교하여 매우 경쟁력 있는 알고리즘이라는 것을 실험을통해 보여준다. 왜냐하면 VSIDS 상태 독립적이기 때문이다.
이 알고리즘은 유지비용이 저렴하다. VSIDS 수백만개의 variable이 있는 문제에 대한 decision 연산에서 매우적은 비율의 실행시간을 점유한다는 것을 실험을 통해 보여 주었다.

보다 최근에, VSIDS에 아이디어를 더 추가한 형태인 "BerkMin: a Fast and Robust SAT-Solver," 알고리즘이 Goldberg and Y. Novikov 에 의해 제안되었다
이 알고리즘은 VSIDS처럼 “active recently" 한 variable 들 중에서 결정하기 위한 decision strategy 이다. VSIDS에서 variable의 활동성은 literal들의 발생(occurrence)과 관련한 score에 의해 평가된다. BerkMin 의 제안자인 Goldberg and Y. Novikov는 conflict가 발생하였을 경우, conflict에 책임이 있는 모든 clause의 모든 literal에 대해서 score를 증가시킨다
정리하자면, zchaff 는 confilct 시점에서 conflict의 장본인 격인 literal이 포함된 clause에 대해서 score를 증가시키지만, BerkMin은 conflict으로 인해 생성된 모든 clause에 대해 scroe를 증가시킨다(차이점)
zchaff와 BerkMin 은 둘다 “recent"에 중점을 두고 있다는 것을, 주기적으로 score를 감쇠시킴(상수 값으로 나눔 zchaff -> 2, BerkMin -> 4)으로써 획득(?)하고 있다.

C. M. Li and Anbulagan은 "Heuristics based on unit propagation for satisfiability problems," 논문에서 branching을 위해 look-ahead(예언능력) heuristic의 사용을 제안하였다.
그리고 O. Dubois and G. Dequen는 "A backbone-search heuristic for efficient solving of hard 3-SAT formulae,"라는 논문에서 branching을 위한 backbone-directed heuristic을 제안하였다.
두 개의 알고리즘 모두 어려운 random problem에 대해서 매우 효율적인 것처럼 보인다는 점에서 특징을 공유한다. 하지만, 그들은 또한 VSIDS에 비해 매우 비싼 연산을 한다.
random sat problem(수학적으로 풀기 어려운 난제)들은 보통 같은 사이즈의 구조화된 문제(structured problem)에 비해 훨씬 어렵다. 현재의 solver들은 오로지 어려운 random 3-sat 문제(수백개의 variable을 갖는)에 대한 공략에 치우쳐 있다.

정리하자면, 현재의 solver들은 작은 규모의 풀기 어려운 random sat에 치우쳐져 있어서, 실제 문제에 대해 적용할 때 너무 비싼 알고리즘이 되버린다. 왜냐하면 실제의 문제들은 보다 큰 규모의 잘 구조화된 문제들이기 때문이다. 그러므로 그러한 알고리즘은 실제 문제를 풀기위해 받아들여질 수 없는 overhead 이다.