bitstringgroupsatisfier.java

来自「Java版的SAT求解器」· Java 代码 · 共 57 行

package positronic.satisfiability.bitstringgroup;

import java.util.Iterator;
import java.util.Set;

import positronic.satisfiability.bitstring.BitStringEqualizer;
import positronic.satisfiability.bitstring.BitStringFixer;
import positronic.satisfiability.bitstring.BitStringPair;
import positronic.satisfiability.bitstring.IBitString;
import positronic.satisfiability.elements.Conjunction;
import positronic.satisfiability.elements.Disjunction;
import positronic.satisfiability.elements.IProblem;
import positronic.satisfiability.elements.Problem;

public class BitStringGroupSatisfier extends Problem implements IProblem
{
	private static final long serialVersionUID = 1L;

	/**
	 * @param args
	 */
	public static void main(String[] args)
	{
		// TODO Auto-generated method stub

	}

	public BitStringGroupSatisfier(IBitStringGroup g,IBitString a,IBitString b,IBitString c) throws Exception
	{
		Set keyset=((BitStringGroup)g).getMap().keySet();
		Iterator it=keyset.iterator();
		while(it.hasNext())
		{
			BitStringPair bsp=(BitStringPair)it.next();
			IBitString left=bsp.getLeft();
			IBitString right=bsp.getRight();
			IBitString lookedup=(IBitString)(((BitStringGroup)g).getMap().get(bsp));
			IProblem newRule=new Conjunction(
					new Conjunction(
					new BitStringFixer(left),
					new BitStringFixer(right),
					new BitStringFixer(lookedup)
					),
					new Conjunction(
					new BitStringEqualizer(a,left),
					new BitStringEqualizer(b,right),
					new BitStringEqualizer(c,lookedup))
					);
			if(this.isEmpty())
				this.setClauses(newRule.getClauses());
			else
				this.setClauses(new Disjunction(this,newRule).getClauses());
		}
	}

}