|
Timetabler
|
Class for representing a set of clauses. More...
#include <clauses.h>
Public Member Functions | |
| Clauses (const std::vector< CClause > &) | |
| Constructs the Clauses object. More... | |
| Clauses (const CClause &) | |
| Constructs the Clauses object. More... | |
| Clauses (const Lit &) | |
| Constructs the Clauses object. More... | |
| Clauses (const Var &) | |
| Constructs the Clauses object. More... | |
| Clauses () | |
| Constructs the Clauses object, with no clauses in it. | |
| Clauses | operator~ () |
| Defines the negation operation on a set of clauses. More... | |
| Clauses | operator & (const Clauses &) |
| Clauses | operator & (const CClause &) |
| Clauses | operator| (const Clauses &) |
| Defines the disjunction operation between two sets of clauses. More... | |
| Clauses | operator| (const CClause &) |
| Defines the disjunction operation between a Clauses and a CClause. More... | |
| Clauses | operator>> (const Clauses &) |
| Defines the implication operation between two sets of Clauses. More... | |
| void | addClauses (const CClause &) |
| Adds a CClause to the set of clauses. More... | |
| void | addClauses (const std::vector< CClause > &) |
| Adds a vector of CClause to the set of clauses. More... | |
| void | addClauses (const Clauses &) |
| Adds the clauses of a Clauses object to this object. More... | |
| std::vector< CClause > | getClauses () const |
| Gets the clauses in this object. More... | |
| void | print () |
| Displays the clauses in this object. | |
| void | clear () |
| Clears the Clauses object by removing all the clauses. | |
Class for representing a set of clauses.
A set of clauses is represented as a vector of type CClause. This class defines operations between sets of clauses, such as AND, OR, NOT, and IMPLIES. This also defines functions to create Clauses, add clauses, and work with them. All clauses are always maintained in the CNF form.
| Clauses::Clauses | ( | const std::vector< CClause > & | clauses | ) |
Constructs the Clauses object.
| [in] | clauses | The clauses in the set of clauses |
Definition at line 17 of file clauses.cpp.
| Clauses::Clauses | ( | const CClause & | clause | ) |
Constructs the Clauses object.
| [in] | clause | A single clause that forms the set of clauses |
Definition at line 26 of file clauses.cpp.
| Clauses::Clauses | ( | const Lit & | lit | ) |
Constructs the Clauses object.
| [in] | lit | A single literal, a Lit, that is converted to a unit clause and forms the set of clauses |
Definition at line 37 of file clauses.cpp.
| Clauses::Clauses | ( | const Var & | var | ) |
Constructs the Clauses object.
| [in] | var | A single variable, a Var, that is converted to a literal with positive polarity, then converted to a unit clause, which then forms the set of clauses |
Definition at line 51 of file clauses.cpp.
| void Clauses::addClauses | ( | const CClause & | other | ) |
Adds a CClause to the set of clauses.
| [in] | other | The CClause to add |
Definition at line 238 of file clauses.cpp.
Referenced by ConstraintAdder::ConstraintAdder(), ConstraintEncoder::hasAtMostOneFieldValueTrue(), ConstraintEncoder::hasSameFieldTypeNotSameValue(), and CClause::operator~().
| void Clauses::addClauses | ( | const std::vector< CClause > & | other | ) |
Adds a vector of CClause to the set of clauses.
| [in] | other | The CClause vector to append |
Definition at line 245 of file clauses.cpp.
| void Clauses::addClauses | ( | const Clauses & | other | ) |
Adds the clauses of a Clauses object to this object.
| [in] | other | The Clauses object whose clauses are to be added |
Definition at line 254 of file clauses.cpp.
References getClauses().
| std::vector< CClause > Clauses::getClauses | ( | ) | const |
Gets the clauses in this object.
Definition at line 264 of file clauses.cpp.
Referenced by addClauses(), Timetabler::addClauses(), operator|(), and CClause::operator~().
Defines the implication operation between two sets of Clauses.
The implication of a set of clauses p to a set of clauses q, which is (p->q), is given by (~p OR q). Thus, this operation is performed using the existing definitions of NOT and OR for sets of clauses.
| other | The Clauses object which is implied by this object |
Definition at line 228 of file clauses.cpp.
Defines the disjunction operation between two sets of clauses.
The disjunction of a set of clauses ((a1 OR a2) AND (b1 OR b2)) with ((x1 OR x2) AND (y1 OR y2)) is given by ((a1 OR a2 OR x1 OR x2) AND (a1 OR a2 OR y1 OR y2) AND (b1 OR b2 OR x1 OR x2) AND (b1 OR b2 OR y1 OR y2)). This function performs this operation and returns a Clauses object with the resultant clauses. Given m clauses in the first operand and n clauses in the second operand, the solution has O(mn) clauses. Using auxiliary variables gives a O(m+n) equisatisfiable formula.
Following is a example with auxiliary variables. ((a1 | a2 | a3 | a4) & (a5 | a6 | ...) & ...) | ((b1 | b2 | b3 | b4) & (b5 | ...) & ...) # Add the following as hard clauses ~x | c1 (c1 is auxiliary variable for (a1 | a2 | a3 | a4)) ... x | ~c1 | c2 | ... ~c1 | a1 | a2 | a3 | a4 c1 | ~a1 c1 | ~a2 ...
x | y
| other | The Clauses object to perform the OR operation with |
Definition at line 149 of file clauses.cpp.
References Timetabler::addClauses(), CClause::addLits(), Timetabler::addToFormula(), getClauses(), Timetabler::newLiteral(), and timetabler.
| Clauses Clauses::operator~ | ( | ) |
Defines the negation operation on a set of clauses.
The negation of a set of clauses ((a1 OR a2) AND (b1 OR b2)) is defined as ((~a1 AND ~a2) OR (~b1 AND ~b2)). The OR operation defined in this class is then used to convert the Clauses to CNF form.
Definition at line 71 of file clauses.cpp.
1.8.13