SAT.Solve

---

Back to table

/*
SAT
SAT.Solve

[binary() result]=SAT.Solve(Dimacs problem, int maxCount=-1);

problem : the source of the problem in the Dimacs format.
maxCount : the number of the solution expected.
result : a list of binary number, indicates the value that satisfies the SAT problem

Solve a SAT problem described in the format of DIMACS.

If maxCount=-1, it returns all the solution.
*/
//-------------------------------------------------------------------
// examples
f=Dimacs()
{
	p cnf 0 0
	-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.Solve(f,2);
Print(result);

//-------------------------------------------------------------------
// result