DefaultConfig returns the default configuration for a SAT solver configuration.

DefaultLowLevelConfig returns a new default configuration of the low-level parameters of the SAT solver.

GenerateNQueens generates an n-queens problem of size n and returns it as a formula.

GeneratePigeonHole generates a pigeon hole problem of size n and returns it as a formula.

HandlerWithTimeout generates a new timeout handler with the given timeout.

Implies reports whether f1 implies f2 (f1 => f2 is always true).

IsContradiction reports whether the formula is a contradiction (always false).

IsEquivalent reports whether f1 is equivalent to f2 (f1 <=> f2 is always true).

IsSatisfiable reports whether the formula is satisfiable.

IsTautology reports whether the formula is a tautology (always true).

MkLit generates a solver literals from a solver variable and sign.

NewCoreSolver generates a new core SAT solver with the given configuration.

NewSolver creates a new SAT solver with the optional configuration.

NewUnitPropagator returns a new unit propagator solver.

Not negates a solver literal.

OptimizationHandlerWithTimeout generates a new timeout handler with the given timeout.

Params generates a new empty call parameter struct with the following default setting: - no handler - no additional formulas or propositions for the SAT call - no model generation for satisfiable formulas - no unsat core computation for unsatisfiable formulas - no computation of propagated literals at decision level 0.

Sign returns if a literal on the solver is negative.

UncheckedEnqueue is the default function to add new variable decisions to the solver.

Vari returns the solver variable of a solver literal.

WithAssumptions generates a new parameter struct with the following setting: - additional assumption literals for the SAT call - no unsat core computation for unsatisfiable formulas - no handler - no model generation for satisfiable formulas - no computation of propagated literals at decision level 0.

WithCore generates a new parameter struct with the following setting: - unsat core computation for unsatisfiable formulas - no handler - no additional formulas or propositions for the SAT call - no model generation for satisfiable formulas - no computation of propagated literals at decision level 0.

WithHandler generates a new parameter struct with the following setting: - use the given handler - no unsat core computation for unsatisfiable formulas - no model generation for satisfiable formulas - no additional assumption literals for the SAT call - no computation of propagated literals at decision level 0.

WithModel generates a new parameter struct with the following setting: - model generation for satisfiable formulas for the given variables - no handler - no additional formulas or propositions for the SAT call - no unsat core computation for unsatisfiable formulas - no computation of propagated literals at decision level 0.

positive, negative and optional variables.

only variables which occur negative in every model.

only variables which occur positive in every model.

simple minimization.

recursive deep minimization.

no clause minimization.

formula factories CNF method.

Plaisted-Greenbaum without NNF generation directly on solver.

Plaisted-Greenbaum with NNF generation directly on solver.

constant for an error state literal.

constant for an undefined literal.

A Backbone of a formula is a set of literals (positive and/or negative) which are present in their respective polarity in every model of the given formula.

CallParams describe the parameters for a single SAT solver call.

CallResult represents the result of a single call to the SAT solver.

Config describes the configuration of a SAT solver.

CoreSolver represents a core SAT solver.

LowLevelConfig describes the low-level parameters of the SAT solver.

A Solver is the main interface an external user should interact with a SAT solver.

A SolverState can be extracted from the solver by the SaveState method and be loaded again with the LoadState method.

A TimeoutHandler can be used to abort a SAT computation depending on a timeout set beforehand.

A TimeoutOptimizationHandler can be used to abort a SAT optimization depending on a timeout set beforehand.

A UnitPropagator is a special solver used for just propagating unit literals on the solver.

DnnfSatSolver is a special solver used for DNNF generation.

Handler is an interface for SAT handlers which can abort the computation based on the number of conflicts found during the computation.

OptimizationHandler is an interface for SAT-based optimizations which can abort the computation everytime a better solution is found during the optimization.

BackboneSort describes sort of backbone should be computed:.

ClauseMinimization encodes the different algorithms for minimizing learnt clauses on the solver.

CNFMethod encodes the different methods for adding formulas as CNF to the solver.