Solving QBF Instances with Nested SAT Solvers

Recent work by Janhunen, Tasharrofi, and Ternovska (2016) started from the following observation: "if SAT From the result of this oracle call, a learned clause is generated and added to ϕ. Now that formalism; (2) It can be immediately combined with other these highly-performant SATsolvers exist, research often SAT extensions (such as integer variables, acyclicity, or any stretches beyond SAT, either because of trying to tackle other theory propagator); (3) No dedicated propagators need problems of a complexity higher than NP or because the input to be developed for the new extension because the nested format of SAT solvers (propositional logic) is too limited solver is (automatically) used as a propagator for its internal to concisely and naturally express certain domain specific theory; for example, it was shown by Janhunen, Tasharrofi, constraints, such as graph properties.