Question

Programs for this problem might preprocess the input by analyzing conditional autarkies. An annual competition for programs solving this problem gives inputs in the DIMACS format (-5[1])and requires outputs in proof formats like DRUP or DRAT. State-of-the-art programs like CaDiCaL and Glucose efficiently solve this problem (-5[1])thanks to a “conflict-driven” technique called CDCL. (15[1])A generalization of this problem “modulo theories” is solved by the Microsoft-developed program (*) Z3. This problem (-5[1])is solved by repeatedly guessing and backtracking while applying unit propagation to resolve single literals in the DPLL algorithm. Solvers for this problem often start by converting the input to conjunctive normal form, which is always (10[1])possible to do using (-5[1])size three clauses. For 10 points, name this problem of deciding if there’s an assignment of variables in a Boolean formula that makes it true. ■END■ (10[2]0[1])

Back to tossups