Plans regarding pseudoboolean constraints.
More...
Go to the source code of this file.
Detailed Description
Plans regarding pseudoboolean constraints.
 Todo:
 The notion of a "pseudoboolean constraint"

Given literals x_1, ..., x_k and integers l, a_1, ..., a_k, u, a pseudoboolean constraint expresses l <= sum_{i=1}^k a_i * x_i <= u, where a satisfied literal means integer 1, a falsified literal means integer 0, and where l, u may also be inf.

Compare "Representing cardinality constraints" in Satisfiability/Lisp/PseudoBoolean/plans/CardinalityConstraints.hpp for the special case where all a_i = 1.

As boolean functions, these are threshold functions as considered in Satisfiability/Lisp/FiniteFunctions/plans/Thresholds.hpp.

Where for cardinality constraint we just had a set L of literals, now we have a list L of literals and a list A of the same length of integers (containing the coefficients).

It just remains the question on the precise composition of the list which represents a pseudoboolean constraint.

One could use lists [l,A,L,u].

The major abbreviation for "pseudoboolean constraint" should be "pbc".
 Todo:
 Application of partial assignments

For a partial assignment and a pbc P=[a,A,L,b] let phi*P be [a',A',L',b], where A', L' are obtained from A resp. L by removing the position corresponding to variables in phi, while a', b' are obtained by arithmetic substitution (and bringing the new constants either to the left or to the right side of the inequality).
 Todo:
 Pseudoboolean constraints as active clauses

See ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/plans/Conditions.hpp and ComputerAlgebra/Satisfiability/Lisp/plans/SatisfactionProblems.hpp for general plans.

See "Pseudoboolean constraints as active clauses" in ComputerAlgebra/Satisfiability/Lisp/PseudoBoolean/plans/CardinalityConstraints.hpp for the special case of cardinality constraints.

Pseudoboolean constraints, and especially cardinality constraint seem good candidates for first "active clauses":

Determining satisfiability and forced assignments w.r.t. a partial assignment should be relatively easy (it is definitely so for cardinality constraints; for pseudoboolean constraints one needs to determine satisfiability of a single integer inequality with {0,1}variables resp. to determine whether some variables have forced values).

Actually, for pbc's we have a knapsackproblem, so the problem here is actually not that easy  we have here an active clauseset!

At least for cardinality constraints we can always determine the corresponding prime implicates representation, and in this way really have "virtual clauses"  via determining the sizes of this representation we can completely emulate the in a sense optimal representation by prime implicates without actually having to create them!
 Todo:
 Add milestones
Definition in file general.hpp.