Encodings of puzzles to CNF, to use as SAT-solver input.
boolExpToCnfScript.sml: Encoding from boolExp to cnf using Tseytin transformation
case_studies: Different puzzles and problems encoded to suitable versatile datatypes.
cnfScript.sml: Definition of CNF
demo: Scripts and example problems for the encoders.
numBoolExpScript.sml: Encode natural numbers to Booleans using order encoding
numBoolExtendedScript.sml: Extend numBoolExp with more functionality
numBoolRangeScript.sml: Add individual upper and lower bounds for each number variable
old_boolExpToCnfScript.sml: Encoding from Boolean expressions to CNF.
orderEncodingBoolScript.sml: Extend pseudoBoolExp with OrderAxiom, to prepare for order encoding of natural numbers.
quantifierExpScript.sml: Quantifiers over Boolean expressions and pseudo-Boolean constraints
translation: Translation scripts for puzzle encodings.
unorderedSetsScript.sml: Encode unordered sets to natural numbers