Tag: autarky
-
Handling disconnected components
In CryptoMiniSat 3.2 and above there is a disconnected component finding&solving system. This finds toplevel disconnected components regularly and solves them by launching an instance of the solver itself. If the component is unsatisfiable (UNSAT), the whole system is UNSAT and solving can be immediately aborted. If the component is satisfiable (SAT) the component’s solution […]
-
Note to self: higher level autarkies
While reading this thesis, I have had a thought about autarkies. Let me first define what an autarky in SAT solving is: A partial assignment phi is called a weak autarky for F if “phi*F is a subset of F” holds, while phi is an autarky for F if phi is a weak autarky for […]