SAT.MaxSAT
Back to table
/*
SAT
SAT.MaxSAT
[list() result]=SAT.MaxSAT(Dimacs problem, int K);
problem : the source of the problem in the Dimacs format.
K : an interger
Solve a MaxSAT(K) problem.
In the worst case, it may list out all the possible solution. Therefore, it may be time-consuming.
*/
//-------------------------------------------------------------------
// examples
f=Dimacs()
{
p cnf 5 19
-1 -2 0
-1 -3 0
-2 -1 0
-2 -3 0
-2 -4 0
-3 -1 0
-3 -2 0
-3 -4 0
-3 -5 0
-4 -2 0
-4 -3 0
-4 -5 0
-5 -3 0
-5 -4 0
1 2 3 0
2 1 3 4 0
3 1 2 4 0
4 2 3 5 0
5 3 4 0
}
[result]=SAT.MaxSAT(f,18);
Print(result);
//-------------------------------------------------------------------
// result
FromBinary List BinaryNumberToString binaryioset() Convert AddXorTerm ToNotFunction ToPOS ToXORP Diagram DigitalSystem ExcitationTable logicvardef minterm Nor MantissaToPositiveNumber Radixes OrAnd POS Save InputVariables CreateCompactTable FastVerificationData Full MultiCover Shannon AdjustLogicVariableCount Substitute Xor Zero
The website is simply translated by using the Google Translate. Please inform us if you find the wrong/funny/weird translation.