OKlibrary  0.2.1.6
general.hpp File Reference

User documentation for the conflict combinatorics of SAT (in Lisp/Maxima) More...

Go to the source code of this file.


Detailed Description

User documentation for the conflict combinatorics of SAT (in Lisp/Maxima)

Hitting clause-sets

See ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac.

Uniform hitting clause-sets

The following properties are equivalent for a uniform clause-set F with clause-length k:

  • F is unsatisfiable and has 2^k clauses
  • F is a hitting clause-set with 2^k clauses
  • F is an unsatisfiable hitting clause-set.

Generators for unsatisfiable uniform hitting clause-sets 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 clause-sets. The first case represents also the only regular unsatisfiable uniform hitting clause-sets.

Definition in file general.hpp.