Source: generators/SATGenerator.js

/**
 * Class for generating SAT problem instances
 */
export class SATGenerator {
  /**
   * Class constructor
   * @param {object} params parameters of the generated instance
   */
  constructor (params) {
    this.params = params;
    this.params.noVariables = +this.params.noVariables;
    this.params.noClauses = +this.params.noClauses;
    this.params.noLiterals = +this.params.noLiterals;
  }

  /**
   * Generate instance based on parameters
   * @return {String} instance of SAT problem coded as String
   */
  generate () {
    var generatedInstance = "p cnf " +  this.params.noVariables + " " + this.params.noClauses + '\n';
    var sign;
    var empty;
    var numberOfClauses = 0;
    var newClause;

    var addedClauses = [];

    while (numberOfClauses !== this.params.noClauses)
    {
      newClause = "";
      empty = true;
      for (var i = 0; i < this.params.noVariables; i++)
      {
        if(Math.random() < 1/(this.params.noVariables / this.params.noLiterals)) {
          sign = Math.round(Math.random());
          if(sign) {
            newClause += (i+1) + " ";
            empty = false;
          }
          else {
            newClause += "-" + (i+1) + " ";
            empty = false;
          }
        }
      }
      if(!empty) {
        newClause += "0" + '\n';
        if(!addedClauses[newClause]){
          numberOfClauses++;
          generatedInstance += newClause;
          addedClauses[newClause] = 1;
        }
      }
    }
    return generatedInstance;
  }
}