Java SATFactory类代码示例

OGeek|极客世界-中国程序员成长平台 › 门户 › 编程› Java›Java编程经验

原作者: [db:作者] 来自: [db:来源] 收藏邀请

本文整理汇总了Java中kodkod.engine.satlab.SATFactory类的典型用法代码示例。如果您正苦于以下问题：Java SATFactory类的具体用法？Java SATFactory怎么用？Java SATFactory使用的例子？那么恭喜您, 这里精选的类代码示例或许可以为您提供帮助。

SATFactory类属于kodkod.engine.satlab包，在下文中一共展示了SATFactory类的20个代码示例，这些例子默认根据受欢迎程度排序。您可以为喜欢或者感觉有用的代码点赞，您的评价将有助于我们的系统推荐出更棒的Java代码示例。

示例1: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.Netconfig [# sites] [# hq] [# routers] [# time
 * steps]
 */
public static void main(String[] args) {
	if (args.length < 4)
		usage();
	final Netconfig model = new Netconfig();
	final Solver solver = new Solver();
	// solver.options().setSolver(SATFactory.ZChaffMincost);
	solver.options().setSolver(SATFactory.MiniSat);
	try {
		final Formula show = model.show();
		final Solution sol = solver.solve(show, model.bounds(Integer.parseInt(args[0]), Integer.parseInt(args[1]),
				Integer.parseInt(args[2]), Integer.parseInt(args[3])));
		// System.out.println(show);
		// System.out.println("p cnf " +
		// (solver.numberOfIntermediateVariables()+solver.numberOfPrimaryVariables())
		// + " " + solver.numberOfClauses());
		System.out.println(sol.outcome());
		System.out.println(sol.stats());

	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:27，代码来源:Netconfig.java

示例2: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.MGT066 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final MGT066 model = new MGT066();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		solver.options().setSymmetryBreaking(n * n);
		final Formula f = model.axioms();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:25，代码来源:MGT066.java

示例3: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.MED007 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final MED007 model = new MED007();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(1000);
		// solver.options().setFlatten(false);
		final Formula f = model.checkTranssls2_qilt27();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:MED007.java

示例4: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: ava examples.tptp.GEO192 [# curves] [# points]
 */
public static void main(String[] args) {
	if (args.length < 2)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);

		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final GEO092 model = new GEO092();
		final Formula f = model.checkProposition2141();

		System.out.println(model.proposition2141());

		final Bounds b = model.bounds(n);
		final Solution sol = solver.solve(f, b);

		System.out.println(sol);
		// System.out.println((new
		// Evaluator(sol.instance())).evaluate(model.axioms().and(model.theorem213().not())));
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:28，代码来源:GEO092.java

示例5: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.GEO191 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);

		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final GEO091 model = new GEO091();
		final Formula f = model.checkTheorem_2_13();

		System.out.println(model.theorem_2_13());

		final Bounds b = model.bounds(n);
		final Solution sol = solver.solve(f, b);

		System.out.println(sol);
		// System.out.println((new
		// Evaluator(sol.instance())).evaluate(model.axioms().and(model.theorem213().not())));
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:28，代码来源:GEO091.java

示例6: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: ava examples.tptp.GEO159 [scope]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);

		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);

		final GEO159 model = new GEO159();
		final Formula f = model.checkDefs();

		final Bounds b = model.bounds(n);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:24，代码来源:GEO159.java

示例7: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.ALG195_1
 */
public static void main(String[] args) {

	try {

		final ALG195_1 model = new ALG195_1();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final Formula f = model.axioms().and(model.co1().not());
		final Bounds b = model.bounds();
		// System.out.println(model.decls());
		// System.out.println(model.ax2ax7());
		// System.out.println(b);
		final Solution sol = solver.solve(f, b);
		if (sol.instance() == null) {
			System.out.println(sol);
		} else {
			System.out.println(sol.stats());
			model.display(sol.instance());
		}
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:27，代码来源:ALG195_1.java

示例8: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.ALG197
 */
public static void main(String[] args) {

	try {

		final ALG197 model = new ALG197();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final Formula f = model.checkCO1();
		final Bounds b = model.bounds();
		final Solution sol = solver.solve(f, b);
		if (sol.instance() == null) {
			System.out.println(sol);
		} else {
			System.out.println(sol.stats());
			model.display(sol.instance());
		}
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:24，代码来源:ALG197.java

示例9: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.COM008 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final COM008 model = new COM008();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(22);
		// solver.options().setFlatten(false);
		final Formula f = model.checkGoalToBeProved();
		final Bounds b = model.bounds(n);
		// System.out.println(f);

		final Solution sol = solver.solve(f, b);
		System.out.println(sol);

	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:28，代码来源:COM008.java

示例10: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.SET967 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final SET967 model = new SET967();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(n*n);
		// solver.options().setFlatten(false);
		final Formula f = model.checkT120_zfmisc_1();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:SET967.java

示例11: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.ALG195
 */
public static void main(String[] args) {

	try {

		final ALG195 model = new ALG195();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final Formula f = model.checkCO1();
		final Bounds b = model.bounds();
		// System.out.println(model.decls());
		// System.out.println(model.ax2ax7());
		// System.out.println(b);
		final Solution sol = solver.solve(f, b);
		if (sol.instance() == null) {
			System.out.println(sol);
		} else {
			System.out.println(sol.stats());
			model.display(sol.instance());
		}
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:27，代码来源:ALG195.java

示例12: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.NUM374 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final NUM374 model = new NUM374();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		solver.options().setSymmetryBreaking(n * n);
		final Formula f = model.checkWilkie();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:25，代码来源:NUM374.java

示例13: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.ALG212 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final ALG212 model = new ALG212();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(n*n);
		// solver.options().setFlatten(false);
		final Formula f = model.checkDistLong();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:ALG212.java

示例14: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.NUM378
 */
public static void main(String[] args) {

	try {

		final NUM378 model = new NUM378();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final Formula f = model.decls().and(model.inequalities());
		final Bounds b = model.bounds();
		// System.out.println(f);
		// System.out.println(b);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol.outcome());
		System.out.println(sol.stats());
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:22，代码来源:NUM378.java

示例15: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.MED009 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final MED009 model = new MED009();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(1000);
		// solver.options().setFlatten(false);
		final Formula f = model.checkTranssls2_qige27();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:MED009.java

示例16: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: ava examples.tptp.GEO115 [scope]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);

		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);

		final GEO115 model = new GEO115();
		final Formula f = model.theorem385();

		final Bounds b = model.bounds(n);
		final Solution sol = solver.solve(f, b);

		System.out.println(sol);

	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:GEO115.java

示例17: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.TOP020 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final TOP020 model = new TOP020();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		final Formula f = model.checkChallenge_AMR_1_4_4();
		final Bounds b = model.bounds(n);
		// System.out.println(f);
		// System.out.println(b);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:25，代码来源:TOP020.java

示例18: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.SET943 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final SET943 model = new SET943();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(1000);
		// solver.options().setFlatten(false);
		final Formula f = model.checkT96_zfmisc_1();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:SET943.java

示例19: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java examples.tptp.SET948 [univ size]
 */
public static void main(String[] args) {
	if (args.length < 1)
		usage();

	try {
		final int n = Integer.parseInt(args[0]);
		if (n < 1)
			usage();
		final SET948 model = new SET948();
		final Solver solver = new Solver();
		solver.options().setSolver(SATFactory.MiniSat);
		// solver.options().setSymmetryBreaking(n*n);
		// solver.options().setFlatten(false);
		final Formula f = model.checkT101_zfmisc_1();
		final Bounds b = model.bounds(n);
		System.out.println(f);
		final Solution sol = solver.solve(f, b);
		System.out.println(sol);
	} catch (NumberFormatException nfe) {
		usage();
	}
}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:26，代码来源:SET948.java

示例20: main

import kodkod.engine.satlab.SATFactory; //导入依赖的package包/类
/**
 * Usage: java tests.Viktor
 */
public static void main(String[] args) {

	final Viktor model = new Viktor();

	final Solver solver = new Solver();
	solver.options().setSolver(SATFactory.MiniSat);
	solver.options().setReporter(new ConsoleReporter());
	solver.options().setBitwidth(7);
	final Formula f = model.checkEquations();
	final Bounds b = model.bounds();
	System.out.println(f);
	System.out.println(b);
	final Solution sol = solver.solve(f, b);

	System.out.println(sol);
	if (sol.instance() != null)
		model.display(sol.instance(), solver.options());

}

开发者ID:AlloyTools，项目名称:org.alloytools.alloy，代码行数:23，代码来源:Viktor.java

注：本文中的kodkod.engine.satlab.SATFactory类示例整理自Github/MSDocs等源码及文档管理平台，相关代码片段筛选自各路编程大神贡献的开源项目，源码版权归原作者所有，传播和使用请参考对应项目的License；未经允许，请勿转载。

鲜花

握手

雷人

路过

鸡蛋

该文章已有0人参与评论

请发表评论

全部评论

专题导读

More+

10-27 六六分期app的软件客服如何联系？(六六分期

11-06 可心卡盟:win10系统火狐flash插件崩溃怎么

11-06 亲亲特价:怎么删除回收站图标

11-06 济南大学虚拟社区:鲁大师节能降温的具体办

11-06 xlueops.exe:无线网络安装向导

11-06 女斗合众国:win7系统cf与主机连接不稳定怎

11-06 0xc000022-[cf烟雾头]cf怎么调烟雾头

11-06 qizideyouhuo:应用程序无法正常启动0xc0000

11-06 ipz-185:win7系统vcf文件怎么打开

11-06 傻哥蹦迪:win10系统s4怎么打开usb调试

11-06 八神浩树gtaste:回收站清空了怎么恢复

11-06 妖尾之黑色守护:win10系统电脑没有1440x900

11-06 校园至尊魔王小说:win7系统浏览网页时字体

11-06 女斗合众国:win10系统访问共享文件夹提示请

11-06 tokyo hot n0654:恢复win7系统默认字体一招

11-06 雨酷仙境:设置win7系统转移临时文件夹腾出

11-06 阿穆纳伊之杖:win7系统开始菜单在右边还原

11-06 tunespotting:win10系统火狐flash插件总是

11-06 甘尔葛分析师：计谋网站seo关键词暴涨有什

11-06 蔡贵霖: 计谋网站seo关键词暴涨有什么秘密

11-06 博益网首页:ao3网页版进入不了解决方法

11-06 漏斗子专栏: 网站数据分析小白易懂精华篇

11-06 见证双虹怎么做:win7系统开启telnet命令的

11-06 颾狐蝶蜋:系统资源不足无法完成请求的服务

11-06 国光中学校歌:提交网站到alexa查询详细步骤

11-06 西安有情天:静态网页和动态网页的区别

11-06 红木雅尚斋:外部链接构造对网站的好处

11-06 前官礼遇：防止域名劫持–增强域安全性的10

11-06 密传二转答案: 中文分词算法有哪些

11-06 金泉家园邮编:百度快照劫持的表现及应对方

Java ExchangeFilterFunction类代码示例发布时间：2022-05-22

Java ByteType类代码示例发布时间：2022-05-22

剪的笔顺,诠释剪的笔画,认识剪的部首

1 六六分期app的软件客服如何联系？(六六分期

六六分期app的软件客服如何联系？不知道吗？加qq群【895510560】即可！标题：六六分期

阅读：18297|2023-10-27

2 可心卡盟:win10系统火狐flash插件崩溃怎么

今天小编告诉大家如何处理win10系统火狐flash插件总是崩溃的问题，可能很多用户都不知

阅读：9687|2022-11-06

3 亲亲特价:怎么删除回收站图标

今天小编告诉大家如何对win10系统删除桌面回收站图标进行设置，可能很多用户都不知道

阅读：8185|2022-11-06

4 济南大学虚拟社区:鲁大师节能降温的具体办

今天小编告诉大家如何对win10系统电脑设置节能降温的设置方法，想必大家都遇到过需要

阅读：8554|2022-11-06

5 xlueops.exe:无线网络安装向导

我们在使用xp系统的过程中,经常需要对xp系统无线网络安装向导设置进行设置，可能很多

阅读：8463|2022-11-06

6 女斗合众国:win7系统cf与主机连接不稳定怎

今天小编告诉大家如何处理win7系统玩cf老是与主机连接不稳定的问题，可能很多用户都不

阅读：9400|2022-11-06

7 0xc000022-[cf烟雾头]cf怎么调烟雾头

电脑对日常生活的重要性小编就不多说了，可是一旦碰到win7系统设置cf烟雾头的问题，很

阅读：8435|2022-11-06

8 qizideyouhuo:应用程序无法正常启动0xc0000

我们在日常使用电脑的时候，有的小伙伴们可能在打开应用的时候会遇见提示应用程序无法

阅读：7869|2022-11-06

9 ipz-185:win7系统vcf文件怎么打开

今天小编告诉大家如何对win7系统打开vcf文件进行设置，可能很多用户都不知道怎么对win

阅读：8420|2022-11-06

10 傻哥蹦迪:win10系统s4怎么打开usb调试

今天小编告诉大家如何对win10系统s4开启USB调试模式进行设置，可能很多用户都不知道怎

阅读：7398|2022-11-06

客服电话

电子邮件

Java SATFactory类代码示例

示例1: main

示例2: main

示例3: main

示例4: main

示例5: main

示例6: main

示例7: main

示例8: main

示例9: main

示例10: main

示例11: main

示例12: main

示例13: main

示例14: main

示例15: main

示例16: main

示例17: main

示例18: main

示例19: main

示例20: main

请发表评论

全部评论

上一篇：

下一篇：

微信小程序自定义组件的坑之 hidden、boole

librespeed/speedtest: Self-hosted Speedt

CVE-2022-0250

avehtari/BDA_m_demos: Bayesian Data Anal

四维彩超怎么看性别？四维看男孩女孩诀窍

剪的笔顺,诠释剪的笔画,认识剪的部首

六六分期app的软件客服如何联系？(六六分期

florent37/ViewAnimator: A fluent Android

florent37/Shrine-MaterialDesign2: implem

CVE-2020-36276

SimpleSoftwareIO/simple-sms: Send and re

关于我们

产品与服务

解决方案

139-2527-9053