Class Instance

Inheritance Relationships

Derived Type

Class Documentation

class Instance

Subclassed by Solver

Protected Functions

void unSet(LiteralID lit)
Antecedent &getAntecedent(LiteralID lit)
const Antecedent &antecedent(LiteralID lit) const

Accessor the antecedent object. It is a constant alternative to the method getAntecedent(LiteralID).

Return
Variable corresponding to the literal.
Parameters
  • lit: Literal identification number

bool hasAntecedent(LiteralID lit) const

Checks if the literal has an antecedent clause.

Return
True if the literal has an antecedent.
Parameters
  • lit: Literal identification object

bool isAntecedentOf(ClauseOfs ante_cl, LiteralID lit)
bool isolated(VariableIndex v)
bool free(VariableIndex v)
bool deleteConflictClauses(bool delete_all = false)
bool markClauseDeleted(ClauseOfs cl_ofs)
void compactConflictLiteralPool()
void compactClauses()
void compactVariables()
void cleanClause(ClauseOfs cl_ofs)

instance.cpp

Purpose: Defines the methods for the Instance() class.

Copyright (C) 2018 Zayd Hammoudeh. All rights reserved.

Author
Zayd Hammoudeh zayd@ucsc.edu
Version
0.00.00

This software may be modified and distributed under the terms of the MIT license. See the LICENSE file for details.

Original Author: Marc Thurley.

unsigned long num_conflict_clauses() const
const VariableIndex num_variables() const

Number of variables in the formula.

Return
Size of the variables array

bool createfromFile(const std::string &file_name)

Reads the CNF formula from a file. It does minimal analysis of the clauses. It adds the clauses to the basic clause data structures including the occurence lists.

If there is a self contradictory clause, it may catch that failure but it is not guaranted.

Return
”true” if the file was parsed and the formula properly built.
Parameters
  • file_name: Location of the CNF formula in a file

void decayActivities()

Decay the activity scores of the literal based on a regular decision frequency (128 decisions in the original code).

void updateActivities(ClauseOfs clause_ofs)
bool isUnitClause(const LiteralID lit)

Checks whether the specified literal is unit clause.

Return
True if the literal is a unit clause.
Parameters
  • lit: Literal identification object.

bool existsUnitClauseOf(VariableIndex v)

Checks whether a unit clause exists for the specified variable.

Return
true if the specified variable is in a unit clause.
Parameters

void ParseCnfCommentForSupport(std::ifstream &input_file)

Parses a comment line in a DIMACs file to extract the independent support if it is present.

Parameters
  • input_file: Input file stream of a DIMACs file.

bool addUnitClause(const LiteralID lit)

Attempts to add a unit clause literal to the set of unit clauses.

If the unit clause (or its complement) already exists, the function merely returns and does nothing.

Return
True if the literal was added or already exists in the unit clause list A return of false implies the formula is UNSAT.
Parameters
  • lit: Unit clause literal

long addClause(std::vector<LiteralID> &literals)

Adds a clause (be it unit, binary, or long) to the set of clauses for the formula.

Return
Identification number of the clause. If there is an error adding the clause, it returns “INT_MIN” (i.e., the minimum integer value).
Parameters
  • literals: Set of literals in the clause

Antecedent addUIPConflictClause(std::vector<LiteralID> &literals)
bool addBinaryClause(LiteralID litA, LiteralID litB)
Variable &var(const LiteralID lit)

Accessor to get a variable object from a literal.

Return
Variable object associated with the literal
Parameters
  • lit: Literal identification object.

const Variable &var_const(const LiteralID lit) const

Const Version of the Variable Function.

Return
Variable object associated with the literal
Parameters
  • lit: Literal identification object.

Literal &literal(LiteralID lit)

Accessor to extract the specified literal.

Return
Literal with the specified ID
Parameters
  • lit: Identification number for a positive or negative literal.

bool isSatisfied(const LiteralID &lit) const
bool isResolved(LiteralID lit)
bool isActive(LiteralID lit) const

Return
true if the variable is unset.
Parameters

std::vector<LiteralID>::const_iterator beginOf(ClauseOfs cl_ofs) const
std::vector<LiteralID>::iterator beginOf(ClauseOfs cl_ofs)
decltype(literal_pool_.begin()) conflict_clauses_begin()
ClauseHeader &getHeaderOf(ClauseOfs cl_ofs)
bool isSatisfied(ClauseOfs cl_ofs)

Protected Attributes

DataAndStatistics statistics_
std::vector<LiteralID> literal_pool_

literal_pool_: the literals of all clauses are stored here INVARIANT: first and last entries of literal_pool_ are a SENTINEL_LIT

Clauses begin with a ClauseHeader structure followed by the literals terminated by SENTINEL_LIT

unsigned long original_lit_pool_size_

this is to determine the starting offset of conflict clauses - MT

This contains the number of unique literals that appear in the original formula. It will be less than or equal to 2 * |variables_|

LiteralIndexedVector<Literal> literals_
LiteralIndexedVector<std::vector<ClauseOfs>> occurrence_lists_

Set of long clauses that the specified literal appears in.

std::vector<ClauseOfs> conflict_clauses_
std::vector<LiteralID> unit_clauses_

Set of all unit clauses (i.e., list of unit literals)

std::vector<Variable> variables_
LiteralIndexedVector<TriValue> literal_values_
std::vector<VariableIndex> unused_vars_

Stores the variable identification numbers of any variables that do not appear in a formula at all.

bool has_independent_support_ = false

Stores whether the solver has an independent support. This is based on the contents of the CNF file.

std::vector<VariableIndex> independent_support

Variables that represent the independent support.