Wonderings of a SAT geek

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 […]