CODEWITHSUNDEEP
boolean-logicxorsolverpropagationsatisfiability
random-user
random-user

Reputation: 47

Native XOR-Support: xor-DPLL(to_examine)

pseudo code of the xor-DPLL

Does anyone here understand the code and is able to answer a few of my question towards it?

For info: to_examine is a queue and saves variables which are recently assigned. var is obviously a variable, it's going to be examined whether it causes a conflict, a propagation or nothing.

What I don't understand is how DPLL(var) is returning a clause in line 3, I thought DPLL can just return true or false.

And how/why does the DPLL algorithm accepts just a single variable in line 3?

The source of this pseudo code is the PHD thesis of Mate Soos from 2009.

Upvotes: 1

Views: 142

Answers (0)

Related Questions