OKlibrary
0.2.1.6

User documentation for the conflict combinatorics of SAT (in Lisp/Maxima) More...
Go to the source code of this file.
User documentation for the conflict combinatorics of SAT (in Lisp/Maxima)
See ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac.
The following properties are equivalent for a uniform clauseset F with clauselength k:
Generators for unsatisfiable uniform hitting clausesets with given k:
uniform_usat_hitting_min
creates the (up to renaming unique elements with minimal deficiency 1 (i.e., maximal number of variables 2^k  1). uniform_usat_hitting_max
creates the (up to renaming unique elements with maximal deficiency 2^k  k (i.e., minimal number of variables k). In both cases we have actually tree hitting clausesets. The first case represents also the only regular unsatisfiable uniform hitting clausesets.
Definition in file general.hpp.