import { BitArray } from "./configurationTypes/BitArray";
import { Problem, ProblemTypeEnum } from './Problem';
// common SAT input
class Literal {
constructor(name, i) {
this.id = name; // int
this.inv = i; // boolean "inverted"
}
}
class Clause {
constructor(literalArray) {
this.literals = literalArray.map(literal => {
let inv = (literal < 0);
let id = inv ? -literal : +literal;
return new Literal(id - 1, inv);
});
}
check(bitArray) {
for (let literal of this.literals) {
if (bitArray[literal.id] && !literal.inv) return true;
if (!bitArray[literal.id] && literal.inv) return true;
}
return false;
}
}
export class SAT extends Problem {
constructor(data) {
super();
this._clauses = [];
let dataSet = data
.split('\n')
.filter(row => row.trim()[0] !== 'c');
let params = dataSet[0]
.split(/(\s+)/)
.filter(x => x.trim().length > 0)
.splice(2, 2)
.map(param => +param);
this.params = {
numberOfVariables: params[0],
numberOfClauses: params[1]
}
dataSet = dataSet
.splice(1, params[1])
.map(row => {
row = row
.trim()
.split(' ');
row = row
.splice(0, row.length - 1)
.map(number => +number);
return row;
});
for (let row in dataSet) {
this._clauses.push(new Clause(dataSet[row]));
};
}
_check(bitArray) {
return this._clauses.reduce((sum, clause) => {
return (clause.check(bitArray)) ? sum + 1 : sum;
}, 0);
}
/**
* Returns fitness of selected configuration(BitArray)
* @param {class} bitArrayConfig BitArray of which fitness we want
* @return {int} calculated fitness of the configuration
*/
evaluateMaximizationCost(bitArrayConfig) {
if (bitArrayConfig === null) return -1;
const bitArray = bitArrayConfig.getBitArray();
return this._check(bitArray);
}
transformMaximizationToRealCost(maxCost) {
return maxCost;
}
/**
* Returns random, or all 0, configuration of SAT problem(BitArray configuration)
* @param {bool} random random or all 0
* @return {class} new BitArray class
*/
getConfiguration(random) {
return new BitArray({
size: this.params.numberOfVariables,
random: random
});
}
/**
* Returns the result of the config, in this case the config array
* @param {class} bitArrayConfig the configuration of which result we want
* @return {Array} the bit array of the configuration
*/
getResult(bitArrayConfig) {
return bitArrayConfig.getBitArray();
}
getType() {
return ProblemTypeEnum.BINARY;
}
/**
* Returns instance invalidity
* @param {string} instanceContent content of the instance
* @return {boolean} is instance invalid
*/
static isInvalidInstance(instanceContent) {
let rows = instanceContent.split('\n').filter(row => row.trim()[0] !== 'c');
let [noVariables, noClauses] = rows[0]
.split(/(\s+)/)
.filter(x => x.trim().length > 0)
.splice(2, 2)
.map(param => +param);
if (isNaN(noVariables) || isNaN(noClauses)) return { text: "Invalid number of parameters" };
if(noVariables < 0) return { text: "Number of variables cant be negative" };
if(noClauses < 0) return { text: "Number of clauses cant be negative" };
if(noClauses > Math.pow(3, noVariables) - 1) return { text: "Number of clauses is at max: " + Math.pow(3, noVariables) - 1 };
rows = rows.slice(1).filter(row => !!row.trim());
let clausesEndIndex = rows.findIndex(row => row.indexOf("%") !== -1);
if (clausesEndIndex === -1) clausesEndIndex = rows.length;
instanceContent = rows
.slice(0, clausesEndIndex)
.join('\n')
.split(/\s+/);
if (noClauses !== clausesEndIndex) return { text: "Number of clauses doesn't match the actual number of clauses" };
let clauses = [];
let clause = "";
if (instanceContent.some(isNaN)) {
// if some elements returns true when isNaN function applied on it
return { text: `Must contain only numbers, except for "p cnf" statement and comments` };
}
for(let i = 0; i < instanceContent.length; i++) {
if(noVariables < +instanceContent[i] || -noVariables > +instanceContent[i]) return { text: `Invalid variable in clause: "${+instanceContent[i]}"` };
if(+instanceContent[i] !== 0) clause += instanceContent[i] + " ";
else {
if(clauses[clause]) return { text: `Multiple same clauses: "${clause} 0"`};
clauses[clause] = 1;
clause = "";
}
}
return false; // valid instance
}
/**
* Returns parameters of the instance
* @param {string} instanceContent content of the instance
* @return {object} instance parameters
*/
static resolveInstanceParams(instanceContent) {
let dataSet = instanceContent
.split('\n')
.filter(row => row.trim()[0] !== 'c');
let params = dataSet[0]
.split(/(\s+)/)
.filter(x => x.trim().length > 0)
.splice(2, 2)
.map(param => +param);
return {
noVariables: params[0],
noClauses: params[1]
}
}
}